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

Metamath Proof Explorer

Theorem mhpval

Description: Value of the "homogeneous polynomial" function. (Contributed by Steven Nguyen, 25-Aug-2023)

Ref Expression
Hypotheses mhpfval.h 
|- H = ( I mHomP R )
mhpfval.p 
|- P = ( I mPoly R )
mhpfval.b 
|- B = ( Base ` P )
mhpfval.0 
|- .0. = ( 0g ` R )
mhpfval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
mhpfval.i 
|- ( ph -> I e. V )
mhpfval.r 
|- ( ph -> R e. W )
mhpval.n 
|- ( ph -> N e. NN0 )
Assertion mhpval 
|- ( ph -> ( H ` N ) = { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } )

Proof

Step Hyp Ref Expression
1 mhpfval.h 
 |-  H = ( I mHomP R )
2 mhpfval.p 
 |-  P = ( I mPoly R )
3 mhpfval.b 
 |-  B = ( Base ` P )
4 mhpfval.0 
 |-  .0. = ( 0g ` R )
5 mhpfval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6 mhpfval.i 
 |-  ( ph -> I e. V )
7 mhpfval.r 
 |-  ( ph -> R e. W )
8 mhpval.n 
 |-  ( ph -> N e. NN0 )
9 1 2 3 4 5 6 7 mhpfval 
 |-  ( ph -> H = ( n e. NN0 |-> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )
10 eqeq2 
 |-  ( n = N -> ( ( ( CCfld |`s NN0 ) gsum g ) = n <-> ( ( CCfld |`s NN0 ) gsum g ) = N ) )
11 10 rabbidv 
 |-  ( n = N -> { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
12 11 sseq2d 
 |-  ( n = N -> ( ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } <-> ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) )
13 12 rabbidv 
 |-  ( n = N -> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } = { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } )
14 13 adantl 
 |-  ( ( ph /\ n = N ) -> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } = { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } )
15 3 fvexi 
 |-  B e. _V
16 15 rabex 
 |-  { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } e. _V
17 16 a1i 
 |-  ( ph -> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } e. _V )
18 9 14 8 17 fvmptd 
 |-  ( ph -> ( H ` N ) = { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } )