Metamath Proof Explorer

Theorem ismhp3

Description: A polynomial is homogeneous iff the degree of every nonzero term is the same. (Contributed by SN, 22-Jul-2024)

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 )
ismhp2.1 
|- ( ph -> X e. B )
Assertion ismhp3 
|- ( ph -> ( X e. ( H ` N ) <-> A. d e. D ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = 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 ismhp2.1 
 |-  ( ph -> X e. B )
10 1 2 3 4 5 6 7 8 ismhp 
 |-  ( ph -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) )
11 9 biantrurd 
 |-  ( ph -> ( ( X 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 } ) ) )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 2 12 3 5 9 mplelf 
 |-  ( ph -> X : D --> ( Base ` R ) )
14 13 ffnd 
 |-  ( ph -> X Fn D )
15 4 fvexi 
 |-  .0. e. _V
16 15 a1i 
 |-  ( ph -> .0. e. _V )
17 elsuppfng 
 |-  ( ( X Fn D /\ X e. B /\ .0. e. _V ) -> ( d e. ( X supp .0. ) <-> ( d e. D /\ ( X ` d ) =/= .0. ) ) )
18 14 9 16 17 syl3anc 
 |-  ( ph -> ( d e. ( X supp .0. ) <-> ( d e. D /\ ( X ` d ) =/= .0. ) ) )
19 oveq2 
 |-  ( g = d -> ( ( CCfld |`s NN0 ) gsum g ) = ( ( CCfld |`s NN0 ) gsum d ) )
20 19 eqeq1d 
 |-  ( g = d -> ( ( ( CCfld |`s NN0 ) gsum g ) = N <-> ( ( CCfld |`s NN0 ) gsum d ) = N ) )
21 20 elrab 
 |-  ( d e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } <-> ( d e. D /\ ( ( CCfld |`s NN0 ) gsum d ) = N ) )
22 21 a1i 
 |-  ( ph -> ( d e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } <-> ( d e. D /\ ( ( CCfld |`s NN0 ) gsum d ) = N ) ) )
23 18 22 imbi12d 
 |-  ( ph -> ( ( d e. ( X supp .0. ) -> d e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) <-> ( ( d e. D /\ ( X ` d ) =/= .0. ) -> ( d e. D /\ ( ( CCfld |`s NN0 ) gsum d ) = N ) ) ) )
24 imdistan 
 |-  ( ( d e. D -> ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = N ) ) <-> ( ( d e. D /\ ( X ` d ) =/= .0. ) -> ( d e. D /\ ( ( CCfld |`s NN0 ) gsum d ) = N ) ) )
25 23 24 bitr4di 
 |-  ( ph -> ( ( d e. ( X supp .0. ) -> d e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) <-> ( d e. D -> ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = N ) ) ) )
26 25 albidv 
 |-  ( ph -> ( A. d ( d e. ( X supp .0. ) -> d e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) <-> A. d ( d e. D -> ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = N ) ) ) )
27 dfss2 
 |-  ( ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } <-> A. d ( d e. ( X supp .0. ) -> d e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) )
28 df-ral 
 |-  ( A. d e. D ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = N ) <-> A. d ( d e. D -> ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = N ) ) )
29 26 27 28 3bitr4g 
 |-  ( ph -> ( ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } <-> A. d e. D ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = N ) ) )
30 10 11 29 3bitr2d 
 |-  ( ph -> ( X e. ( H ` N ) <-> A. d e. D ( ( X ` d ) =/= .0. -> ( ( CCfld |`s NN0 ) gsum d ) = N ) ) )