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

Step	Hyp	Ref	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 𝑓
8	7	cv 1474	. . . . . . 7 class 𝑓
9	3	cv 1474	. . . . . . . 8 class 𝑟
10		c0g 15923	. . . . . . . 8 class 0g
11	9, 10	cfv 5804	. . . . . . 7 class (0g‘𝑟)
12		csupp 7182	. . . . . . 7 class supp
13	8, 11, 12	co 6549	. . . . . 6 class (𝑓 supp (0g‘𝑟))
14		vj	. . . . . . . . . . 11 setvar 𝑗
15	14	cv 1474	. . . . . . . . . 10 class 𝑗
16		vg	. . . . . . . . . . 11 setvar 𝑔
17	16	cv 1474	. . . . . . . . . 10 class 𝑔
18	15, 17	cfv 5804	. . . . . . . . 9 class (𝑔‘𝑗)
19	6, 18, 14	csu 14264	. . . . . . . 8 class Σ𝑗 ∈ ℕ0 (𝑔‘𝑗)
20	5	cv 1474	. . . . . . . 8 class 𝑛
21	19, 20	wceq 1475	. . . . . . 7 wff Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛
22		vh	. . . . . . . . . . . 12 setvar ℎ
23	22	cv 1474	. . . . . . . . . . 11 class ℎ
24	23	ccnv 5037	. . . . . . . . . 10 class ◡ℎ
25		cn 10897	. . . . . . . . . 10 class ℕ
26	24, 25	cima 5041	. . . . . . . . 9 class (◡ℎ “ ℕ)
27		cfn 7841	. . . . . . . . 9 class Fin
28	26, 27	wcel 1977	. . . . . . . 8 wff (◡ℎ “ ℕ) ∈ Fin
29	2	cv 1474	. . . . . . . . 9 class 𝑖
30		cmap 7744	. . . . . . . . 9 class ↑𝑚
31	6, 29, 30	co 6549	. . . . . . . 8 class (ℕ0 ↑𝑚 𝑖)
32	28, 22, 31	crab 2900	. . . . . . 7 class {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
33	21, 16, 32	crab 2900	. . . . . 6 class {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}
34	13, 33	wss 3540	. . . . 5 wff (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}
35		cmpl 19174	. . . . . . 7 class mPoly
36	29, 9, 35	co 6549	. . . . . 6 class (𝑖 mPoly 𝑟)
37		cbs 15695	. . . . . 6 class Base
38	36, 37	cfv 5804	. . . . 5 class (Base‘(𝑖 mPoly 𝑟))
39	34, 7, 38	crab 2900	. . . 4 class {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}}
40	5, 6, 39	cmpt 4643	. . 3 class (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}})
41	2, 3, 4, 4, 40	cmpt2 6551	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}}))
42	1, 41	wceq 1475	1 wff mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}}))

This definition is referenced by: (None)