This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( 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 } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmhp 
 |-  mHomP
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vn 
 |-  n
5 cn0 
 |-  NN0
6 vf 
 |-  f
7 cbs 
 |-  Base
8 1 cv 
 |-  i
9 cmpl 
 |-  mPoly
10 3 cv 
 |-  r
11 8 10 9 co 
 |-  ( i mPoly r )
12 11 7 cfv 
 |-  ( Base ` ( i mPoly r ) )
13 6 cv 
 |-  f
14 csupp 
 |-  supp
15 c0g 
 |-  0g
16 10 15 cfv 
 |-  ( 0g ` r )
17 13 16 14 co 
 |-  ( f supp ( 0g ` r ) )
18 vg 
 |-  g
19 vh 
 |-  h
20 cmap 
 |-  ^m
21 5 8 20 co 
 |-  ( NN0 ^m i )
22 19 cv 
 |-  h
23 22 ccnv 
 |-  `' h
24 cn 
 |-  NN
25 23 24 cima 
 |-  ( `' h " NN )
26 cfn 
 |-  Fin
27 25 26 wcel 
 |-  ( `' h " NN ) e. Fin
28 27 19 21 crab 
 |-  { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
29 ccnfld 
 |-  CCfld
30 cress 
 |-  |`s
31 29 5 30 co 
 |-  ( CCfld |`s NN0 )
32 cgsu 
 |-  gsum
33 18 cv 
 |-  g
34 31 33 32 co 
 |-  ( ( CCfld |`s NN0 ) gsum g )
35 4 cv 
 |-  n
36 34 35 wceq 
 |-  ( ( CCfld |`s NN0 ) gsum g ) = n
37 36 18 28 crab 
 |-  { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n }
38 17 37 wss 
 |-  ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n }
39 38 6 12 crab 
 |-  { f e. ( Base ` ( i mPoly r ) ) | ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } }
40 4 5 39 cmpt 
 |-  ( 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 } | ( ( CCfld |`s NN0 ) gsum g ) = n } } )
41 1 3 2 2 40 cmpo 
 |-  ( 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 } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )
42 0 41 wceq 
 |-  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 } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )