Metamath Proof Explorer

Theorem coeaddlem

Description: Lemma for coeadd and dgradd . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses coefv0.1 
|- A = ( coeff ` F )
coeadd.2 
|- B = ( coeff ` G )
coeadd.3 
|- M = ( deg ` F )
coeadd.4 
|- N = ( deg ` G )
Assertion coeaddlem 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF + G ) ) = ( A oF + B ) /\ ( deg ` ( F oF + G ) ) <_ if ( M <_ N , N , M ) ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 
 |-  A = ( coeff ` F )
2 coeadd.2 
 |-  B = ( coeff ` G )
3 coeadd.3 
 |-  M = ( deg ` F )
4 coeadd.4 
 |-  N = ( deg ` G )
5 plyaddcl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF + G ) e. ( Poly ` CC ) )
6 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
7 4 6 eqeltrid 
 |-  ( G e. ( Poly ` S ) -> N e. NN0 )
8 7 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> N e. NN0 )
9 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
10 3 9 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> M e. NN0 )
11 10 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> M e. NN0 )
12 8 11 ifcld 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> if ( M <_ N , N , M ) e. NN0 )
13 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
14 13 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
15 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
16 15 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> A : NN0 --> CC )
17 2 coef3 
 |-  ( G e. ( Poly ` S ) -> B : NN0 --> CC )
18 17 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> B : NN0 --> CC )
19 nn0ex 
 |-  NN0 e. _V
20 19 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> NN0 e. _V )
21 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
22 14 16 18 20 20 21 off 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( A oF + B ) : NN0 --> CC )
23 oveq12 
 |-  ( ( ( A ` k ) = 0 /\ ( B ` k ) = 0 ) -> ( ( A ` k ) + ( B ` k ) ) = ( 0 + 0 ) )
24 00id 
 |-  ( 0 + 0 ) = 0
25 23 24 eqtrdi 
 |-  ( ( ( A ` k ) = 0 /\ ( B ` k ) = 0 ) -> ( ( A ` k ) + ( B ` k ) ) = 0 )
26 16 ffnd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> A Fn NN0 )
27 18 ffnd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> B Fn NN0 )
28 eqidd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( A ` k ) = ( A ` k ) )
29 eqidd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( B ` k ) = ( B ` k ) )
30 26 27 20 20 21 28 29 ofval 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( A oF + B ) ` k ) = ( ( A ` k ) + ( B ` k ) ) )
31 30 eqeq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( ( A oF + B ) ` k ) = 0 <-> ( ( A ` k ) + ( B ` k ) ) = 0 ) )
32 25 31 imbitrrid 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( ( A ` k ) = 0 /\ ( B ` k ) = 0 ) -> ( ( A oF + B ) ` k ) = 0 ) )
33 32 necon3ad 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( ( A oF + B ) ` k ) =/= 0 -> -. ( ( A ` k ) = 0 /\ ( B ` k ) = 0 ) ) )
34 neorian 
 |-  ( ( ( A ` k ) =/= 0 \/ ( B ` k ) =/= 0 ) <-> -. ( ( A ` k ) = 0 /\ ( B ` k ) = 0 ) )
35 33 34 imbitrrdi 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( ( A oF + B ) ` k ) =/= 0 -> ( ( A ` k ) =/= 0 \/ ( B ` k ) =/= 0 ) ) )
36 1 3 dgrub2 
 |-  ( F e. ( Poly ` S ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
37 36 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
38 plyco0 
 |-  ( ( M e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ M ) ) )
39 11 16 38 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ M ) ) )
40 37 39 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ M ) )
41 40 r19.21bi 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ M ) )
42 11 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> M e. NN0 )
43 42 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> M e. RR )
44 8 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> N e. NN0 )
45 44 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> N e. RR )
46 max1 
 |-  ( ( M e. RR /\ N e. RR ) -> M <_ if ( M <_ N , N , M ) )
47 43 45 46 syl2anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> M <_ if ( M <_ N , N , M ) )
48 nn0re 
 |-  ( k e. NN0 -> k e. RR )
49 48 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> k e. RR )
50 12 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> if ( M <_ N , N , M ) e. NN0 )
51 50 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> if ( M <_ N , N , M ) e. RR )
52 letr 
 |-  ( ( k e. RR /\ M e. RR /\ if ( M <_ N , N , M ) e. RR ) -> ( ( k <_ M /\ M <_ if ( M <_ N , N , M ) ) -> k <_ if ( M <_ N , N , M ) ) )
53 49 43 51 52 syl3anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( k <_ M /\ M <_ if ( M <_ N , N , M ) ) -> k <_ if ( M <_ N , N , M ) ) )
54 47 53 mpan2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( k <_ M -> k <_ if ( M <_ N , N , M ) ) )
55 41 54 syld 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ if ( M <_ N , N , M ) ) )
56 2 4 dgrub2 
 |-  ( G e. ( Poly ` S ) -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
57 56 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
58 plyco0 
 |-  ( ( N e. NN0 /\ B : NN0 --> CC ) -> ( ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( B ` k ) =/= 0 -> k <_ N ) ) )
59 8 18 58 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( B ` k ) =/= 0 -> k <_ N ) ) )
60 57 59 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> A. k e. NN0 ( ( B ` k ) =/= 0 -> k <_ N ) )
61 60 r19.21bi 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( B ` k ) =/= 0 -> k <_ N ) )
62 max2 
 |-  ( ( M e. RR /\ N e. RR ) -> N <_ if ( M <_ N , N , M ) )
63 43 45 62 syl2anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> N <_ if ( M <_ N , N , M ) )
64 letr 
 |-  ( ( k e. RR /\ N e. RR /\ if ( M <_ N , N , M ) e. RR ) -> ( ( k <_ N /\ N <_ if ( M <_ N , N , M ) ) -> k <_ if ( M <_ N , N , M ) ) )
65 49 45 51 64 syl3anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( k <_ N /\ N <_ if ( M <_ N , N , M ) ) -> k <_ if ( M <_ N , N , M ) ) )
66 63 65 mpan2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( k <_ N -> k <_ if ( M <_ N , N , M ) ) )
67 61 66 syld 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( B ` k ) =/= 0 -> k <_ if ( M <_ N , N , M ) ) )
68 55 67 jaod 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( ( A ` k ) =/= 0 \/ ( B ` k ) =/= 0 ) -> k <_ if ( M <_ N , N , M ) ) )
69 35 68 syld 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. NN0 ) -> ( ( ( A oF + B ) ` k ) =/= 0 -> k <_ if ( M <_ N , N , M ) ) )
70 69 ralrimiva 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> A. k e. NN0 ( ( ( A oF + B ) ` k ) =/= 0 -> k <_ if ( M <_ N , N , M ) ) )
71 plyco0 
 |-  ( ( if ( M <_ N , N , M ) e. NN0 /\ ( A oF + B ) : NN0 --> CC ) -> ( ( ( A oF + B ) " ( ZZ>= ` ( if ( M <_ N , N , M ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( A oF + B ) ` k ) =/= 0 -> k <_ if ( M <_ N , N , M ) ) ) )
72 12 22 71 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( ( A oF + B ) " ( ZZ>= ` ( if ( M <_ N , N , M ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( A oF + B ) ` k ) =/= 0 -> k <_ if ( M <_ N , N , M ) ) ) )
73 70 72 mpbird 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( A oF + B ) " ( ZZ>= ` ( if ( M <_ N , N , M ) + 1 ) ) ) = { 0 } )
74 simpl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F e. ( Poly ` S ) )
75 simpr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G e. ( Poly ` S ) )
76 1 3 coeid 
 |-  ( F e. ( Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
77 76 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
78 2 4 coeid 
 |-  ( G e. ( Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
79 78 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
80 74 75 11 8 16 18 37 57 77 79 plyaddlem1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF + G ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) ) )
81 5 12 22 73 80 coeeq 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF + G ) ) = ( A oF + B ) )
82 elfznn0 
 |-  ( k e. ( 0 ... if ( M <_ N , N , M ) ) -> k e. NN0 )
83 ffvelcdm 
 |-  ( ( ( A oF + B ) : NN0 --> CC /\ k e. NN0 ) -> ( ( A oF + B ) ` k ) e. CC )
84 22 82 83 syl2an 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ k e. ( 0 ... if ( M <_ N , N , M ) ) ) -> ( ( A oF + B ) ` k ) e. CC )
85 5 12 84 80 dgrle 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF + G ) ) <_ if ( M <_ N , N , M ) )
86 81 85 jca 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF + G ) ) = ( A oF + B ) /\ ( deg ` ( F oF + G ) ) <_ if ( M <_ N , N , M ) ) )