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

Metamath Proof Explorer

Theorem ismhp

Description: Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023)

Ref Expression
Hypotheses ismhp.h 
|- H = ( I mHomP R )
ismhp.p 
|- P = ( I mPoly R )
ismhp.b 
|- B = ( Base ` P )
ismhp.0 
|- .0. = ( 0g ` R )
ismhp.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
ismhp.n 
|- ( ph -> N e. NN0 )
Assertion ismhp 
|- ( ph -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) )

Proof

Step Hyp Ref Expression
1 ismhp.h 
 |-  H = ( I mHomP R )
2 ismhp.p 
 |-  P = ( I mPoly R )
3 ismhp.b 
 |-  B = ( Base ` P )
4 ismhp.0 
 |-  .0. = ( 0g ` R )
5 ismhp.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6 ismhp.n 
 |-  ( ph -> N e. NN0 )
7 reldmmhp 
 |-  Rel dom mHomP
8 id 
 |-  ( X e. ( H ` N ) -> X e. ( H ` N ) )
9 7 1 8 elfvov1 
 |-  ( X e. ( H ` N ) -> I e. _V )
10 7 1 8 elfvov2 
 |-  ( X e. ( H ` N ) -> R e. _V )
11 9 10 jca 
 |-  ( X e. ( H ` N ) -> ( I e. _V /\ R e. _V ) )
12 11 anim2i 
 |-  ( ( ph /\ X e. ( H ` N ) ) -> ( ph /\ ( I e. _V /\ R e. _V ) ) )
13 reldmmpl 
 |-  Rel dom mPoly
14 13 2 3 elbasov 
 |-  ( X e. B -> ( I e. _V /\ R e. _V ) )
15 14 adantr 
 |-  ( ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( I e. _V /\ R e. _V ) )
16 15 anim2i 
 |-  ( ( ph /\ ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) -> ( ph /\ ( I e. _V /\ R e. _V ) ) )
17 simprl 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> I e. _V )
18 simprr 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> R e. _V )
19 6 adantr 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> N e. NN0 )
20 1 2 3 4 5 17 18 19 mhpval 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> ( H ` N ) = { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } )
21 20 eleq2d 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> ( X e. ( H ` N ) <-> X e. { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } ) )
22 oveq1 
 |-  ( f = X -> ( f supp .0. ) = ( X supp .0. ) )
23 22 sseq1d 
 |-  ( f = X -> ( ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } <-> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) )
24 23 elrab 
 |-  ( X e. { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) )
25 21 24 bitrdi 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) )
26 12 16 25 pm5.21nd 
 |-  ( ph -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) )