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 21676
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 21672 . 2 class mHomP
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3475 . . 3 class V
5 vn . . . 4 setvar 𝑛
6 cn0 12472 . . . 4 class 0
7 vf . . . . . . . 8 setvar 𝑓
87cv 1541 . . . . . . 7 class 𝑓
93cv 1541 . . . . . . . 8 class 𝑟
10 c0g 17385 . . . . . . . 8 class 0g
119, 10cfv 6544 . . . . . . 7 class (0g𝑟)
12 csupp 8146 . . . . . . 7 class supp
138, 11, 12co 7409 . . . . . 6 class (𝑓 supp (0g𝑟))
14 ccnfld 20944 . . . . . . . . . 10 class fld
15 cress 17173 . . . . . . . . . 10 class s
1614, 6, 15co 7409 . . . . . . . . 9 class (ℂflds0)
17 vg . . . . . . . . . 10 setvar 𝑔
1817cv 1541 . . . . . . . . 9 class 𝑔
19 cgsu 17386 . . . . . . . . 9 class Σg
2016, 18, 19co 7409 . . . . . . . 8 class ((ℂflds0) Σg 𝑔)
215cv 1541 . . . . . . . 8 class 𝑛
2220, 21wceq 1542 . . . . . . 7 wff ((ℂflds0) Σg 𝑔) = 𝑛
23 vh . . . . . . . . . . . 12 setvar
2423cv 1541 . . . . . . . . . . 11 class
2524ccnv 5676 . . . . . . . . . 10 class
26 cn 12212 . . . . . . . . . 10 class
2725, 26cima 5680 . . . . . . . . 9 class ( “ ℕ)
28 cfn 8939 . . . . . . . . 9 class Fin
2927, 28wcel 2107 . . . . . . . 8 wff ( “ ℕ) ∈ Fin
302cv 1541 . . . . . . . . 9 class 𝑖
31 cmap 8820 . . . . . . . . 9 class m
326, 30, 31co 7409 . . . . . . . 8 class (ℕ0m 𝑖)
3329, 23, 32crab 3433 . . . . . . 7 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
3422, 17, 33crab 3433 . . . . . 6 class {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}
3513, 34wss 3949 . . . . 5 wff (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}
36 cmpl 21459 . . . . . . 7 class mPoly
3730, 9, 36co 7409 . . . . . 6 class (𝑖 mPoly 𝑟)
38 cbs 17144 . . . . . 6 class Base
3937, 38cfv 6544 . . . . 5 class (Base‘(𝑖 mPoly 𝑟))
4035, 7, 39crab 3433 . . . 4 class {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}}
415, 6, 40cmpt 5232 . . 3 class (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}})
422, 3, 4, 4, 41cmpo 7411 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g𝑟)) ⊆ {𝑔 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑛}}))
431, 42wceq 1542 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  21682
  Copyright terms: Public domain W3C validator