Metamath Proof Explorer


Theorem mdeg0

Description: Degree of the zero polynomial. (Contributed by Stefan O'Rear, 20-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdeg0.d
|- D = ( I mDeg R )
mdeg0.p
|- P = ( I mPoly R )
mdeg0.z
|- .0. = ( 0g ` P )
Assertion mdeg0
|- ( ( I e. V /\ R e. Ring ) -> ( D ` .0. ) = -oo )

Proof

Step Hyp Ref Expression
1 mdeg0.d
 |-  D = ( I mDeg R )
2 mdeg0.p
 |-  P = ( I mPoly R )
3 mdeg0.z
 |-  .0. = ( 0g ` P )
4 ringgrp
 |-  ( R e. Ring -> R e. Grp )
5 2 mplgrp
 |-  ( ( I e. V /\ R e. Grp ) -> P e. Grp )
6 4 5 sylan2
 |-  ( ( I e. V /\ R e. Ring ) -> P e. Grp )
7 eqid
 |-  ( Base ` P ) = ( Base ` P )
8 7 3 grpidcl
 |-  ( P e. Grp -> .0. e. ( Base ` P ) )
9 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
10 eqid
 |-  { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } = { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin }
11 eqid
 |-  ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) = ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) )
12 1 2 7 9 10 11 mdegval
 |-  ( .0. e. ( Base ` P ) -> ( D ` .0. ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( .0. supp ( 0g ` R ) ) ) , RR* , < ) )
13 6 8 12 3syl
 |-  ( ( I e. V /\ R e. Ring ) -> ( D ` .0. ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( .0. supp ( 0g ` R ) ) ) , RR* , < ) )
14 simpl
 |-  ( ( I e. V /\ R e. Ring ) -> I e. V )
15 4 adantl
 |-  ( ( I e. V /\ R e. Ring ) -> R e. Grp )
16 2 10 9 3 14 15 mpl0
 |-  ( ( I e. V /\ R e. Ring ) -> .0. = ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { ( 0g ` R ) } ) )
17 fvex
 |-  ( 0g ` R ) e. _V
18 fnconstg
 |-  ( ( 0g ` R ) e. _V -> ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { ( 0g ` R ) } ) Fn { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } )
19 17 18 mp1i
 |-  ( ( I e. V /\ R e. Ring ) -> ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { ( 0g ` R ) } ) Fn { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } )
20 16 fneq1d
 |-  ( ( I e. V /\ R e. Ring ) -> ( .0. Fn { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } <-> ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { ( 0g ` R ) } ) Fn { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } ) )
21 19 20 mpbird
 |-  ( ( I e. V /\ R e. Ring ) -> .0. Fn { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } )
22 ovex
 |-  ( NN0 ^m I ) e. _V
23 22 rabex
 |-  { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } e. _V
24 23 a1i
 |-  ( ( I e. V /\ R e. Ring ) -> { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } e. _V )
25 17 a1i
 |-  ( ( I e. V /\ R e. Ring ) -> ( 0g ` R ) e. _V )
26 fnsuppeq0
 |-  ( ( .0. Fn { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } /\ { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } e. _V /\ ( 0g ` R ) e. _V ) -> ( ( .0. supp ( 0g ` R ) ) = (/) <-> .0. = ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { ( 0g ` R ) } ) ) )
27 21 24 25 26 syl3anc
 |-  ( ( I e. V /\ R e. Ring ) -> ( ( .0. supp ( 0g ` R ) ) = (/) <-> .0. = ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { ( 0g ` R ) } ) ) )
28 16 27 mpbird
 |-  ( ( I e. V /\ R e. Ring ) -> ( .0. supp ( 0g ` R ) ) = (/) )
29 28 imaeq2d
 |-  ( ( I e. V /\ R e. Ring ) -> ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( .0. supp ( 0g ` R ) ) ) = ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " (/) ) )
30 ima0
 |-  ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " (/) ) = (/)
31 29 30 eqtrdi
 |-  ( ( I e. V /\ R e. Ring ) -> ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( .0. supp ( 0g ` R ) ) ) = (/) )
32 31 supeq1d
 |-  ( ( I e. V /\ R e. Ring ) -> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( .0. supp ( 0g ` R ) ) ) , RR* , < ) = sup ( (/) , RR* , < ) )
33 xrsup0
 |-  sup ( (/) , RR* , < ) = -oo
34 32 33 eqtrdi
 |-  ( ( I e. V /\ R e. Ring ) -> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( .0. supp ( 0g ` R ) ) ) , RR* , < ) = -oo )
35 13 34 eqtrd
 |-  ( ( I e. V /\ R e. Ring ) -> ( D ` .0. ) = -oo )