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

Metamath Proof Explorer

Theorem mhpfval

Description: Value of the "homogeneous polynomial" operator. (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 )
Assertion mhpfval 
|- ( ph -> H = ( n e. NN0 |-> { 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 6 elexd 
 |-  ( ph -> I e. _V )
9 7 elexd 
 |-  ( ph -> R e. _V )
10 oveq12 
 |-  ( ( i = I /\ r = R ) -> ( i mPoly r ) = ( I mPoly R ) )
11 10 2 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( i mPoly r ) = P )
12 11 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPoly r ) ) = ( Base ` P ) )
13 12 3 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPoly r ) ) = B )
14 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
15 14 4 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
16 15 oveq2d 
 |-  ( r = R -> ( f supp ( 0g ` r ) ) = ( f supp .0. ) )
17 16 adantl 
 |-  ( ( i = I /\ r = R ) -> ( f supp ( 0g ` r ) ) = ( f supp .0. ) )
18 oveq2 
 |-  ( i = I -> ( NN0 ^m i ) = ( NN0 ^m I ) )
19 18 rabeqdv 
 |-  ( i = I -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
20 19 5 eqtr4di 
 |-  ( i = I -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
21 20 rabeqdv 
 |-  ( i = I -> { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } )
22 21 adantr 
 |-  ( ( i = I /\ r = R ) -> { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } )
23 17 22 sseq12d 
 |-  ( ( i = I /\ r = R ) -> ( ( f supp ( 0g ` r ) ) C_ { g e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } <-> ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } ) )
24 13 23 rabeqbidv 
 |-  ( ( i = I /\ r = R ) -> { 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 } } = { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } )
25 24 mpteq2dv 
 |-  ( ( i = I /\ r = R ) -> ( 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 } } ) = ( n e. NN0 |-> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )
26 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 } } ) )
27 nn0ex 
 |-  NN0 e. _V
28 27 mptex 
 |-  ( n e. NN0 |-> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) e. _V
29 25 26 28 ovmpoa 
 |-  ( ( I e. _V /\ R e. _V ) -> ( I mHomP R ) = ( n e. NN0 |-> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )
30 8 9 29 syl2anc 
 |-  ( ph -> ( I mHomP R ) = ( n e. NN0 |-> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )
31 1 30 eqtrid 
 |-  ( ph -> H = ( n e. NN0 |-> { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )