Definition df-mhp 22437

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 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}))

Distinct variable group:   𝑓,𝑔,ℎ,𝑖,𝑛,𝑟

Detailed syntax breakdown of Definition df-mhp

Step	Hyp	Ref	Expression
1		cmhp 22434	. 2 class mHomP
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3451	. . 3 class V
5		vn	. . . 4 setvar 𝑛
6		cn0 12587	. . . 4 class ℕ0
7		vf	. . . . . . . 8 setvar 𝑓
8	7	cv 1569	. . . . . . 7 class 𝑓
9	3	cv 1569	. . . . . . . 8 class 𝑟
10		c0g 17590	. . . . . . . 8 class 0g
11	9, 10	cfv 6531	. . . . . . 7 class (0g‘𝑟)
12		csupp 8161	. . . . . . 7 class supp
13	8, 11, 12	co 7412	. . . . . 6 class (𝑓 supp (0g‘𝑟))
14		ccnfld 21658	. . . . . . . . . 10 class ℂfld
15		cress 17388	. . . . . . . . . 10 class ↾s
16	14, 6, 15	co 7412	. . . . . . . . 9 class (ℂfld ↾s ℕ0)
17		vg	. . . . . . . . . 10 setvar 𝑔
18	17	cv 1569	. . . . . . . . 9 class 𝑔
19		cgsu 17591	. . . . . . . . 9 class Σg
20	16, 18, 19	co 7412	. . . . . . . 8 class ((ℂfld ↾s ℕ0) Σg 𝑔)
21	5	cv 1569	. . . . . . . 8 class 𝑛
22	20, 21	wceq 1570	. . . . . . 7 wff ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛
23		vh	. . . . . . . . . . . 12 setvar ℎ
24	23	cv 1569	. . . . . . . . . . 11 class ℎ
25	24	ccnv 5650	. . . . . . . . . 10 class ◡ℎ
26		cn 12316	. . . . . . . . . 10 class ℕ
27	25, 26	cima 5654	. . . . . . . . 9 class (◡ℎ “ ℕ)
28		cfn 8957	. . . . . . . . 9 class Fin
29	27, 28	wcel 2145	. . . . . . . 8 wff (◡ℎ “ ℕ) ∈ Fin
30	2	cv 1569	. . . . . . . . 9 class 𝑖
31		cmap 8831	. . . . . . . . 9 class ↑m
32	6, 30, 31	co 7412	. . . . . . . 8 class (ℕ0 ↑m 𝑖)
33	29, 23, 32	crab 3413	. . . . . . 7 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
34	22, 17, 33	crab 3413	. . . . . 6 class {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}
35	13, 34	wss 3899	. . . . 5 wff (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}
36		cmpl 22194	. . . . . . 7 class mPoly
37	30, 9, 36	co 7412	. . . . . 6 class (𝑖 mPoly 𝑟)
38		cbs 17367	. . . . . 6 class Base
39	37, 38	cfv 6531	. . . . 5 class (Base‘(𝑖 mPoly 𝑟))
40	35, 7, 39	crab 3413	. . . 4 class {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}
41	5, 6, 40	cmpt 5186	. . 3 class (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}})
42	2, 3, 4, 4, 41	cmpo 7414	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}))
43	1, 42	wceq 1570	1 wff mHomP = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑛}}))

This definition is used by:  reldmmhp  22438  mhpfval  22439