Definition df-mhp

Description: Define the subspaces of order- n homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	df-mhp	⊢ mHomP = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmhp	⊢ mHomP
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vr	⊢ 𝑟
4		vn	⊢ 𝑛
5		cn0	⊢ ℕ0
6		vf	⊢ 𝑓
7		cbs	⊢ Base
8	1	cv	⊢ 𝑖
9		cmpl	⊢ mPoly
10	3	cv	⊢ 𝑟
11	8 10 9	co	⊢ ( 𝑖 mPoly 𝑟 )
12	11 7	cfv	⊢ ( Base ‘ ( 𝑖 mPoly 𝑟 ) )
13	6	cv	⊢ 𝑓
14		csupp	⊢ supp
15		c0g	⊢ 0g
16	10 15	cfv	⊢ ( 0g ‘ 𝑟 )
17	13 16 14	co	⊢ ( 𝑓 supp ( 0g ‘ 𝑟 ) )
18		vg	⊢ 𝑔
19		vh	⊢ ℎ
20		cmap	⊢ ↑m
21	5 8 20	co	⊢ ( ℕ0 ↑m 𝑖 )
22	19	cv	⊢ ℎ
23	22	ccnv	⊢ ◡ ℎ
24		cn	⊢ ℕ
25	23 24	cima	⊢ ( ◡ ℎ “ ℕ )
26		cfn	⊢ Fin
27	25 26	wcel	⊢ ( ◡ ℎ “ ℕ ) ∈ Fin
28	27 19 21	crab	⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
29		ccnfld	⊢ ℂfld
30		cress	⊢ ↾s
31	29 5 30	co	⊢ ( ℂfld ↾s ℕ0 )
32		cgsu	⊢ Σg
33	18	cv	⊢ 𝑔
34	31 33 32	co	⊢ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 )
35	4	cv	⊢ 𝑛
36	34 35	wceq	⊢ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛
37	36 18 28	crab	⊢ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 }
38	17 37	wss	⊢ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 }
39	38 6 12	crab	⊢ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } }
40	4 5 39	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } )
41	1 3 2 2 40	cmpo	⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
42	0 41	wceq	⊢ mHomP = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )