Metamath Proof Explorer

Theorem mdegaddle

Description: The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses mdegaddle.y 
|- Y = ( I mPoly R )
mdegaddle.d 
|- D = ( I mDeg R )
mdegaddle.i 
|- ( ph -> I e. V )
mdegaddle.r 
|- ( ph -> R e. Ring )
mdegaddle.b 
|- B = ( Base ` Y )
mdegaddle.p 
|- .+ = ( +g ` Y )
mdegaddle.f 
|- ( ph -> F e. B )
mdegaddle.g 
|- ( ph -> G e. B )
Assertion mdegaddle 
|- ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )

Proof

Step Hyp Ref Expression
1 mdegaddle.y 
 |-  Y = ( I mPoly R )
2 mdegaddle.d 
 |-  D = ( I mDeg R )
3 mdegaddle.i 
 |-  ( ph -> I e. V )
4 mdegaddle.r 
 |-  ( ph -> R e. Ring )
5 mdegaddle.b 
 |-  B = ( Base ` Y )
6 mdegaddle.p 
 |-  .+ = ( +g ` Y )
7 mdegaddle.f 
 |-  ( ph -> F e. B )
8 mdegaddle.g 
 |-  ( ph -> G e. B )
9 eqid 
 |-  ( +g ` R ) = ( +g ` R )
10 1 5 9 6 7 8 mpladd 
 |-  ( ph -> ( F .+ G ) = ( F oF ( +g ` R ) G ) )
11 10 fveq1d 
 |-  ( ph -> ( ( F .+ G ) ` c ) = ( ( F oF ( +g ` R ) G ) ` c ) )
12 11 adantr 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( F .+ G ) ` c ) = ( ( F oF ( +g ` R ) G ) ` c ) )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 eqid 
 |-  { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
15 1 13 5 14 7 mplelf 
 |-  ( ph -> F : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> ( Base ` R ) )
16 15 ffnd 
 |-  ( ph -> F Fn { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
17 16 adantr 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> F Fn { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
18 1 13 5 14 8 mplelf 
 |-  ( ph -> G : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> ( Base ` R ) )
19 18 ffnd 
 |-  ( ph -> G Fn { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
20 19 adantr 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> G Fn { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
21 ovex 
 |-  ( NN0 ^m I ) e. _V
22 21 rabex 
 |-  { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } e. _V
23 22 a1i 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } e. _V )
24 simpr 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
25 fnfvof 
 |-  ( ( ( F Fn { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ G Fn { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) /\ ( { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } e. _V /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) ) -> ( ( F oF ( +g ` R ) G ) ` c ) = ( ( F ` c ) ( +g ` R ) ( G ` c ) ) )
26 17 20 23 24 25 syl22anc 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( F oF ( +g ` R ) G ) ` c ) = ( ( F ` c ) ( +g ` R ) ( G ` c ) ) )
27 12 26 eqtrd 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( F .+ G ) ` c ) = ( ( F ` c ) ( +g ` R ) ( G ` c ) ) )
28 27 adantrr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( F .+ G ) ` c ) = ( ( F ` c ) ( +g ` R ) ( G ` c ) ) )
29 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
30 eqid 
 |-  ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) = ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) )
31 7 adantr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> F e. B )
32 simprl 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
33 2 1 5 mdegxrcl 
 |-  ( F e. B -> ( D ` F ) e. RR* )
34 7 33 syl 
 |-  ( ph -> ( D ` F ) e. RR* )
35 34 adantr 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( D ` F ) e. RR* )
36 2 1 5 mdegxrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
37 8 36 syl 
 |-  ( ph -> ( D ` G ) e. RR* )
38 37 34 ifcld 
 |-  ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* )
39 38 adantr 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* )
40 nn0ssre 
 |-  NN0 C_ RR
41 ressxr 
 |-  RR C_ RR*
42 40 41 sstri 
 |-  NN0 C_ RR*
43 14 30 tdeglem1 
 |-  ( I e. V -> ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> NN0 )
44 3 43 syl 
 |-  ( ph -> ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> NN0 )
45 44 ffvelrnda 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) e. NN0 )
46 42 45 sseldi 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) e. RR* )
47 35 39 46 3jca 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( D ` F ) e. RR* /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) e. RR* ) )
48 47 adantrr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( D ` F ) e. RR* /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) e. RR* ) )
49 xrmax1 
 |-  ( ( ( D ` F ) e. RR* /\ ( D ` G ) e. RR* ) -> ( D ` F ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
50 34 37 49 syl2anc 
 |-  ( ph -> ( D ` F ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
51 50 adantr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( D ` F ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
52 simprr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) )
53 51 52 jca 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( D ` F ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) )
54 xrlelttr 
 |-  ( ( ( D ` F ) e. RR* /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) e. RR* ) -> ( ( ( D ` F ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) -> ( D ` F ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) )
55 48 53 54 sylc 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( D ` F ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) )
56 2 1 5 29 14 30 31 32 55 mdeglt 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( F ` c ) = ( 0g ` R ) )
57 8 adantr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> G e. B )
58 37 adantr 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( D ` G ) e. RR* )
59 58 39 46 3jca 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( D ` G ) e. RR* /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) e. RR* ) )
60 59 adantrr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( D ` G ) e. RR* /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) e. RR* ) )
61 xrmax2 
 |-  ( ( ( D ` F ) e. RR* /\ ( D ` G ) e. RR* ) -> ( D ` G ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
62 34 37 61 syl2anc 
 |-  ( ph -> ( D ` G ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
63 62 adantr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( D ` G ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
64 63 52 jca 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( D ` G ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) )
65 xrlelttr 
 |-  ( ( ( D ` G ) e. RR* /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) e. RR* ) -> ( ( ( D ` G ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) -> ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) )
66 60 64 65 sylc 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) )
67 2 1 5 29 14 30 57 32 66 mdeglt 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( G ` c ) = ( 0g ` R ) )
68 56 67 oveq12d 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( F ` c ) ( +g ` R ) ( G ` c ) ) = ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) )
69 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
70 4 69 syl 
 |-  ( ph -> R e. Grp )
71 13 29 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
72 4 71 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
73 13 9 29 grplid 
 |-  ( ( R e. Grp /\ ( 0g ` R ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
74 70 72 73 syl2anc 
 |-  ( ph -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
75 74 adantr 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
76 68 75 eqtrd 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( F ` c ) ( +g ` R ) ( G ` c ) ) = ( 0g ` R ) )
77 28 76 eqtrd 
 |-  ( ( ph /\ ( c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) ) ) -> ( ( F .+ G ) ` c ) = ( 0g ` R ) )
78 77 expr 
 |-  ( ( ph /\ c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) -> ( ( F .+ G ) ` c ) = ( 0g ` R ) ) )
79 78 ralrimiva 
 |-  ( ph -> A. c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) -> ( ( F .+ G ) ` c ) = ( 0g ` R ) ) )
80 1 mplring 
 |-  ( ( I e. V /\ R e. Ring ) -> Y e. Ring )
81 3 4 80 syl2anc 
 |-  ( ph -> Y e. Ring )
82 5 6 ringacl 
 |-  ( ( Y e. Ring /\ F e. B /\ G e. B ) -> ( F .+ G ) e. B )
83 81 7 8 82 syl3anc 
 |-  ( ph -> ( F .+ G ) e. B )
84 2 1 5 29 14 30 mdegleb 
 |-  ( ( ( F .+ G ) e. B /\ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* ) -> ( ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) <-> A. c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) -> ( ( F .+ G ) ` c ) = ( 0g ` R ) ) ) )
85 83 38 84 syl2anc 
 |-  ( ph -> ( ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) <-> A. c e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` c ) -> ( ( F .+ G ) ` c ) = ( 0g ` R ) ) ) )
86 79 85 mpbird 
 |-  ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )