Definition df-mhp 19541

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

Assertion

Ref	Expression
df-mhp	|- mHomP = ( i e. _V , r e. _V |-> ( n e. NN0 |-> { f e. ( Base ` ( i mPoly r ) ) | ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | sum_ j e. NN0 ( g ` j ) = n } } ) )

Distinct variable group:   f, g, h, i, j, n, r

Detailed syntax breakdown of Definition df-mhp

Step	Hyp	Ref	Expression
1		cmhp 19537	. 2 class mHomP
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5		vn	. . . 4 setvar n
6		cn0 11292	. . . 4 class NN0
7		vf	. . . . . . . 8 setvar f
8	7	cv 1482	. . . . . . 7 class f
9	3	cv 1482	. . . . . . . 8 class r
10		c0g 16100	. . . . . . . 8 class 0g
11	9, 10	cfv 5888	. . . . . . 7 class ( 0g ` r )
12		csupp 7295	. . . . . . 7 class supp
13	8, 11, 12	co 6650	. . . . . 6 class ( f supp ( 0g ` r ) )
14		vj	. . . . . . . . . . 11 setvar j
15	14	cv 1482	. . . . . . . . . 10 class j
16		vg	. . . . . . . . . . 11 setvar g
17	16	cv 1482	. . . . . . . . . 10 class g
18	15, 17	cfv 5888	. . . . . . . . 9 class ( g ` j )
19	6, 18, 14	csu 14416	. . . . . . . 8 class sum_ j e. NN0 ( g ` j )
20	5	cv 1482	. . . . . . . 8 class n
21	19, 20	wceq 1483	. . . . . . 7 wff sum_ j e. NN0 ( g ` j ) = n
22		vh	. . . . . . . . . . . 12 setvar h
23	22	cv 1482	. . . . . . . . . . 11 class h
24	23	ccnv 5113	. . . . . . . . . 10 class `' h
25		cn 11020	. . . . . . . . . 10 class NN
26	24, 25	cima 5117	. . . . . . . . 9 class ( `' h " NN )
27		cfn 7955	. . . . . . . . 9 class Fin
28	26, 27	wcel 1990	. . . . . . . 8 wff ( `' h " NN ) e. Fin
29	2	cv 1482	. . . . . . . . 9 class i
30		cmap 7857	. . . . . . . . 9 class ^m
31	6, 29, 30	co 6650	. . . . . . . 8 class ( NN0 ^m i )
32	28, 22, 31	crab 2916	. . . . . . 7 class { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
33	21, 16, 32	crab 2916	. . . . . 6 class { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | sum_ j e. NN0 ( g ` j ) = n }
34	13, 33	wss 3574	. . . . 5 wff ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | sum_ j e. NN0 ( g ` j ) = n }
35		cmpl 19353	. . . . . . 7 class mPoly
36	29, 9, 35	co 6650	. . . . . 6 class ( i mPoly r )
37		cbs 15857	. . . . . 6 class Base
38	36, 37	cfv 5888	. . . . 5 class ( Base ` ( i mPoly r ) )
39	34, 7, 38	crab 2916	. . . 4 class { f e. ( Base ` ( i mPoly r ) ) | ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | sum_ j e. NN0 ( g ` j ) = n } }
40	5, 6, 39	cmpt 4729	. . 3 class ( n e. NN0 |-> { f e. ( Base ` ( i mPoly r ) ) | ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | sum_ j e. NN0 ( g ` j ) = n } } )
41	2, 3, 4, 4, 40	cmpt2 6652	. 2 class ( i e. _V , r e. _V |-> ( n e. NN0 |-> { f e. ( Base ` ( i mPoly r ) ) | ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | sum_ j e. NN0 ( g ` j ) = n } } ) )
42	1, 41	wceq 1483	1 wff mHomP = ( i e. _V , r e. _V |-> ( n e. NN0 |-> { f e. ( Base ` ( i mPoly r ) ) | ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | sum_ j e. NN0 ( g ` j ) = n } } ) )

This definition is referenced by: (None)