Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mhp Structured version   Visualization version   GIF version

Definition df-mhp 19362
 Description: Define the subspaces of order- 𝑛 homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
df-mhp mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔𝑗) = 𝑛}}))
Distinct variable group:   𝑓,𝑔,,𝑖,𝑗,𝑛,𝑟

Detailed syntax breakdown of Definition df-mhp
StepHypRef Expression
1 cmhp 19358 . 2 class mHomP
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3173 . . 3 class V
5 vn . . . 4 setvar 𝑛
6 cn0 11169 . . . 4 class 0
7 vf . . . . . . . 8 setvar 𝑓
87cv 1474 . . . . . . 7 class 𝑓
93cv 1474 . . . . . . . 8 class 𝑟
10 c0g 15923 . . . . . . . 8 class 0g
119, 10cfv 5804 . . . . . . 7 class (0g𝑟)
12 csupp 7182 . . . . . . 7 class supp
138, 11, 12co 6549 . . . . . 6 class (𝑓 supp (0g𝑟))
14 vj . . . . . . . . . . 11 setvar 𝑗
1514cv 1474 . . . . . . . . . 10 class 𝑗
16 vg . . . . . . . . . . 11 setvar 𝑔
1716cv 1474 . . . . . . . . . 10 class 𝑔
1815, 17cfv 5804 . . . . . . . . 9 class (𝑔𝑗)
196, 18, 14csu 14264 . . . . . . . 8 class Σ𝑗 ∈ ℕ0 (𝑔𝑗)
205cv 1474 . . . . . . . 8 class 𝑛
2119, 20wceq 1475 . . . . . . 7 wff Σ𝑗 ∈ ℕ0 (𝑔𝑗) = 𝑛
22 vh . . . . . . . . . . . 12 setvar
2322cv 1474 . . . . . . . . . . 11 class
2423ccnv 5037 . . . . . . . . . 10 class
25 cn 10897 . . . . . . . . . 10 class
2624, 25cima 5041 . . . . . . . . 9 class ( “ ℕ)
27 cfn 7841 . . . . . . . . 9 class Fin
2826, 27wcel 1977 . . . . . . . 8 wff ( “ ℕ) ∈ Fin
292cv 1474 . . . . . . . . 9 class 𝑖
30 cmap 7744 . . . . . . . . 9 class 𝑚
316, 29, 30co 6549 . . . . . . . 8 class (ℕ0𝑚 𝑖)
3228, 22, 31crab 2900 . . . . . . 7 class { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin}
3321, 16, 32crab 2900 . . . . . 6 class {𝑔 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔𝑗) = 𝑛}
3413, 33wss 3540 . . . . 5 wff (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔𝑗) = 𝑛}
35 cmpl 19174 . . . . . . 7 class mPoly
3629, 9, 35co 6549 . . . . . 6 class (𝑖 mPoly 𝑟)
37 cbs 15695 . . . . . 6 class Base
3836, 37cfv 5804 . . . . 5 class (Base‘(𝑖 mPoly 𝑟))
3934, 7, 38crab 2900 . . . 4 class {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔𝑗) = 𝑛}}
405, 6, 39cmpt 4643 . . 3 class (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔𝑗) = 𝑛}})
412, 3, 4, 4, 40cmpt2 6551 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔𝑗) = 𝑛}}))
421, 41wceq 1475 1 wff mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔𝑗) = 𝑛}}))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator