Metamath Proof Explorer


Theorem plyadd

Description: The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014)

Ref Expression
Hypotheses plyadd.1 φ F Poly S
plyadd.2 φ G Poly S
plyadd.3 φ x S y S x + y S
Assertion plyadd φ F + f G Poly S

Proof

Step Hyp Ref Expression
1 plyadd.1 φ F Poly S
2 plyadd.2 φ G Poly S
3 plyadd.3 φ x S y S x + y S
4 elply2 F Poly S S m 0 a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k
5 4 simprbi F Poly S m 0 a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k
6 1 5 syl φ m 0 a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k
7 elply2 G Poly S S n 0 b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k
8 7 simprbi G Poly S n 0 b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k
9 2 8 syl φ n 0 b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k
10 reeanv m 0 n 0 a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k m 0 a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k n 0 b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k
11 reeanv a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k
12 simp1l φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k φ
13 12 1 syl φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k F Poly S
14 12 2 syl φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k G Poly S
15 12 3 sylan φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k x S y S x + y S
16 simp1rl φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k m 0
17 simp1rr φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k n 0
18 simp2l φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k a S 0 0
19 simp2r φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k b S 0 0
20 simp3ll φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k a m + 1 = 0
21 simp3rl φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k b n + 1 = 0
22 simp3lr φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k F = z k = 0 m a k z k
23 oveq1 z = w z k = w k
24 23 oveq2d z = w a k z k = a k w k
25 24 sumeq2sdv z = w k = 0 m a k z k = k = 0 m a k w k
26 fveq2 k = j a k = a j
27 oveq2 k = j w k = w j
28 26 27 oveq12d k = j a k w k = a j w j
29 28 cbvsumv k = 0 m a k w k = j = 0 m a j w j
30 25 29 eqtrdi z = w k = 0 m a k z k = j = 0 m a j w j
31 30 cbvmptv z k = 0 m a k z k = w j = 0 m a j w j
32 22 31 eqtrdi φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k F = w j = 0 m a j w j
33 simp3rr φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k G = z k = 0 n b k z k
34 23 oveq2d z = w b k z k = b k w k
35 34 sumeq2sdv z = w k = 0 n b k z k = k = 0 n b k w k
36 fveq2 k = j b k = b j
37 36 27 oveq12d k = j b k w k = b j w j
38 37 cbvsumv k = 0 n b k w k = j = 0 n b j w j
39 35 38 eqtrdi z = w k = 0 n b k z k = j = 0 n b j w j
40 39 cbvmptv z k = 0 n b k z k = w j = 0 n b j w j
41 33 40 eqtrdi φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k G = w j = 0 n b j w j
42 13 14 15 16 17 18 19 20 21 32 41 plyaddlem φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k F + f G Poly S
43 42 3expia φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k F + f G Poly S
44 43 rexlimdvva φ m 0 n 0 a S 0 0 b S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b n + 1 = 0 G = z k = 0 n b k z k F + f G Poly S
45 11 44 syl5bir φ m 0 n 0 a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k F + f G Poly S
46 45 rexlimdvva φ m 0 n 0 a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k F + f G Poly S
47 10 46 syl5bir φ m 0 a S 0 0 a m + 1 = 0 F = z k = 0 m a k z k n 0 b S 0 0 b n + 1 = 0 G = z k = 0 n b k z k F + f G Poly S
48 6 9 47 mp2and φ F + f G Poly S