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

Definition df-mhp 20788
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𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}}))
Distinct variable group:   𝑓,𝑔,,𝑖,𝑛,𝑟

Detailed syntax breakdown of Definition df-mhp
StepHypRef Expression
1 cmhp 20784 . 2 class mHomP
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3444 . . 3 class V
5 vn . . . 4 setvar 𝑛
6 cn0 11889 . . . 4 class 0
7 vf . . . . . . . 8 setvar 𝑓
87cv 1537 . . . . . . 7 class 𝑓
93cv 1537 . . . . . . . 8 class 𝑟
10 c0g 16708 . . . . . . . 8 class 0g
119, 10cfv 6328 . . . . . . 7 class (0g𝑟)
12 csupp 7817 . . . . . . 7 class supp
138, 11, 12co 7139 . . . . . 6 class (𝑓 supp (0g𝑟))
14 ccnfld 20094 . . . . . . . . . 10 class fld
15 cress 16479 . . . . . . . . . 10 class s
1614, 6, 15co 7139 . . . . . . . . 9 class (ℂflds0)
17 vg . . . . . . . . . 10 setvar 𝑔
1817cv 1537 . . . . . . . . 9 class 𝑔
19 cgsu 16709 . . . . . . . . 9 class Σg
2016, 18, 19co 7139 . . . . . . . 8 class ((ℂflds0) Σg 𝑔)
215cv 1537 . . . . . . . 8 class 𝑛
2220, 21wceq 1538 . . . . . . 7 wff ((ℂflds0) Σg 𝑔) = 𝑛
23 vh . . . . . . . . . . . 12 setvar
2423cv 1537 . . . . . . . . . . 11 class
2524ccnv 5522 . . . . . . . . . 10 class
26 cn 11629 . . . . . . . . . 10 class
2725, 26cima 5526 . . . . . . . . 9 class ( “ ℕ)
28 cfn 8496 . . . . . . . . 9 class Fin
2927, 28wcel 2112 . . . . . . . 8 wff ( “ ℕ) ∈ Fin
302cv 1537 . . . . . . . . 9 class 𝑖
31 cmap 8393 . . . . . . . . 9 class m
326, 30, 31co 7139 . . . . . . . 8 class (ℕ0m 𝑖)
3329, 23, 32crab 3113 . . . . . . 7 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
3422, 17, 33crab 3113 . . . . . 6 class {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}
3513, 34wss 3884 . . . . 5 wff (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}
36 cmpl 20594 . . . . . . 7 class mPoly
3730, 9, 36co 7139 . . . . . 6 class (𝑖 mPoly 𝑟)
38 cbs 16478 . . . . . 6 class Base
3937, 38cfv 6328 . . . . 5 class (Base‘(𝑖 mPoly 𝑟))
4035, 7, 39crab 3113 . . . 4 class {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}}
415, 6, 40cmpt 5113 . . 3 class (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}})
422, 3, 4, 4, 41cmpo 7141 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}}))
431, 42wceq 1538 1 wff mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}}))
Colors of variables: wff setvar class
This definition is referenced by:  mhpfval  20794
  Copyright terms: Public domain W3C validator