Definition df-mhp 19541

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 19537	. 2 class mHomP
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3200	. . 3 class V
5		vn	. . . 4 setvar 𝑛
6		cn0 11292	. . . 4 class ℕ0
7		vf	. . . . . . . 8 setvar 𝑓
8	7	cv 1482	. . . . . . 7 class 𝑓
9	3	cv 1482	. . . . . . . 8 class 𝑟
10		c0g 16100	. . . . . . . 8 class 0g
11	9, 10	cfv 5888	. . . . . . 7 class (0g‘𝑟)
12		csupp 7295	. . . . . . 7 class supp
13	8, 11, 12	co 6650	. . . . . 6 class (𝑓 supp (0g‘𝑟))
14		vj	. . . . . . . . . . 11 setvar 𝑗
15	14	cv 1482	. . . . . . . . . 10 class 𝑗
16		vg	. . . . . . . . . . 11 setvar 𝑔
17	16	cv 1482	. . . . . . . . . 10 class 𝑔
18	15, 17	cfv 5888	. . . . . . . . 9 class (𝑔‘𝑗)
19	6, 18, 14	csu 14416	. . . . . . . 8 class Σ𝑗 ∈ ℕ0 (𝑔‘𝑗)
20	5	cv 1482	. . . . . . . 8 class 𝑛
21	19, 20	wceq 1483	. . . . . . 7 wff Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛
22		vh	. . . . . . . . . . . 12 setvar ℎ
23	22	cv 1482	. . . . . . . . . . 11 class ℎ
24	23	ccnv 5113	. . . . . . . . . 10 class ◡ℎ
25		cn 11020	. . . . . . . . . 10 class ℕ
26	24, 25	cima 5117	. . . . . . . . 9 class (◡ℎ “ ℕ)
27		cfn 7955	. . . . . . . . 9 class Fin
28	26, 27	wcel 1990	. . . . . . . 8 wff (◡ℎ “ ℕ) ∈ Fin
29	2	cv 1482	. . . . . . . . 9 class 𝑖
30		cmap 7857	. . . . . . . . 9 class ↑𝑚
31	6, 29, 30	co 6650	. . . . . . . 8 class (ℕ0 ↑𝑚 𝑖)
32	28, 22, 31	crab 2916	. . . . . . 7 class {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
33	21, 16, 32	crab 2916	. . . . . 6 class {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}
34	13, 33	wss 3574	. . . . 5 wff (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}
35		cmpl 19353	. . . . . . 7 class mPoly
36	29, 9, 35	co 6650	. . . . . 6 class (𝑖 mPoly 𝑟)
37		cbs 15857	. . . . . 6 class Base
38	36, 37	cfv 5888	. . . . 5 class (Base‘(𝑖 mPoly 𝑟))
39	34, 7, 38	crab 2916	. . . 4 class {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}}
40	5, 6, 39	cmpt 4729	. . 3 class (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}})
41	2, 3, 4, 4, 40	cmpt2 6652	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}}))
42	1, 41	wceq 1483	1 wff mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ Σ𝑗 ∈ ℕ0 (𝑔‘𝑗) = 𝑛}}))

This definition is referenced by: (None)