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

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