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 )