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 } ) ) )