Metamath Proof Explorer


Theorem dgrcolem1

Description: The degree of a composition of a monomial with a polynomial. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses dgrcolem1.1 N = deg G
dgrcolem1.2 φ M
dgrcolem1.3 φ N
dgrcolem1.4 φ G Poly S
Assertion dgrcolem1 φ deg x G x M = M N

Proof

Step Hyp Ref Expression
1 dgrcolem1.1 N = deg G
2 dgrcolem1.2 φ M
3 dgrcolem1.3 φ N
4 dgrcolem1.4 φ G Poly S
5 oveq2 y = 1 G x y = G x 1
6 5 mpteq2dv y = 1 x G x y = x G x 1
7 6 fveq2d y = 1 deg x G x y = deg x G x 1
8 oveq1 y = 1 y N = 1 N
9 7 8 eqeq12d y = 1 deg x G x y = y N deg x G x 1 = 1 N
10 9 imbi2d y = 1 φ deg x G x y = y N φ deg x G x 1 = 1 N
11 oveq2 y = d G x y = G x d
12 11 mpteq2dv y = d x G x y = x G x d
13 12 fveq2d y = d deg x G x y = deg x G x d
14 oveq1 y = d y N = d N
15 13 14 eqeq12d y = d deg x G x y = y N deg x G x d = d N
16 15 imbi2d y = d φ deg x G x y = y N φ deg x G x d = d N
17 oveq2 y = d + 1 G x y = G x d + 1
18 17 mpteq2dv y = d + 1 x G x y = x G x d + 1
19 18 fveq2d y = d + 1 deg x G x y = deg x G x d + 1
20 oveq1 y = d + 1 y N = d + 1 N
21 19 20 eqeq12d y = d + 1 deg x G x y = y N deg x G x d + 1 = d + 1 N
22 21 imbi2d y = d + 1 φ deg x G x y = y N φ deg x G x d + 1 = d + 1 N
23 oveq2 y = M G x y = G x M
24 23 mpteq2dv y = M x G x y = x G x M
25 24 fveq2d y = M deg x G x y = deg x G x M
26 oveq1 y = M y N = M N
27 25 26 eqeq12d y = M deg x G x y = y N deg x G x M = M N
28 27 imbi2d y = M φ deg x G x y = y N φ deg x G x M = M N
29 plyf G Poly S G :
30 4 29 syl φ G :
31 30 ffvelrnda φ x G x
32 31 exp1d φ x G x 1 = G x
33 32 mpteq2dva φ x G x 1 = x G x
34 30 feqmptd φ G = x G x
35 33 34 eqtr4d φ x G x 1 = G
36 35 fveq2d φ deg x G x 1 = deg G
37 36 1 syl6eqr φ deg x G x 1 = N
38 3 nncnd φ N
39 38 mulid2d φ 1 N = N
40 37 39 eqtr4d φ deg x G x 1 = 1 N
41 31 adantlr φ d x G x
42 nnnn0 d d 0
43 42 adantl φ d d 0
44 43 adantr φ d x d 0
45 41 44 expp1d φ d x G x d + 1 = G x d G x
46 45 mpteq2dva φ d x G x d + 1 = x G x d G x
47 cnex V
48 47 a1i φ d V
49 ovexd φ d x G x d V
50 eqidd φ d x G x d = x G x d
51 34 adantr φ d G = x G x
52 48 49 41 50 51 offval2 φ d x G x d × f G = x G x d G x
53 46 52 eqtr4d φ d x G x d + 1 = x G x d × f G
54 53 fveq2d φ d deg x G x d + 1 = deg x G x d × f G
55 54 adantr φ d deg x G x d = d N deg x G x d + 1 = deg x G x d × f G
56 oveq1 deg x G x d = d N deg x G x d + N = d N + N
57 56 adantl φ d deg x G x d = d N deg x G x d + N = d N + N
58 eqidd φ d y y d = y y d
59 oveq1 y = G x y d = G x d
60 41 51 58 59 fmptco φ d y y d G = x G x d
61 ssidd φ d
62 1cnd φ d 1
63 plypow 1 d 0 y y d Poly
64 61 62 43 63 syl3anc φ d y y d Poly
65 plyssc Poly S Poly
66 4 adantr φ d G Poly S
67 65 66 sseldi φ d G Poly
68 addcl z w z + w
69 68 adantl φ d z w z + w
70 mulcl z w z w
71 70 adantl φ d z w z w
72 64 67 69 71 plyco φ d y y d G Poly
73 60 72 eqeltrrd φ d x G x d Poly
74 73 adantr φ d deg x G x d = d N x G x d Poly
75 simpr φ d deg x G x d = d N deg x G x d = d N
76 simpr φ d d
77 3 adantr φ d N
78 76 77 nnmulcld φ d d N
79 78 nnne0d φ d d N 0
80 79 adantr φ d deg x G x d = d N d N 0
81 75 80 eqnetrd φ d deg x G x d = d N deg x G x d 0
82 fveq2 x G x d = 0 𝑝 deg x G x d = deg 0 𝑝
83 dgr0 deg 0 𝑝 = 0
84 82 83 syl6eq x G x d = 0 𝑝 deg x G x d = 0
85 84 necon3i deg x G x d 0 x G x d 0 𝑝
86 81 85 syl φ d deg x G x d = d N x G x d 0 𝑝
87 67 adantr φ d deg x G x d = d N G Poly
88 3 nnne0d φ N 0
89 fveq2 G = 0 𝑝 deg G = deg 0 𝑝
90 89 83 syl6eq G = 0 𝑝 deg G = 0
91 1 90 syl5eq G = 0 𝑝 N = 0
92 91 necon3i N 0 G 0 𝑝
93 88 92 syl φ G 0 𝑝
94 93 adantr φ d G 0 𝑝
95 94 adantr φ d deg x G x d = d N G 0 𝑝
96 eqid deg x G x d = deg x G x d
97 96 1 dgrmul x G x d Poly x G x d 0 𝑝 G Poly G 0 𝑝 deg x G x d × f G = deg x G x d + N
98 74 86 87 95 97 syl22anc φ d deg x G x d = d N deg x G x d × f G = deg x G x d + N
99 nncn d d
100 99 adantl φ d d
101 38 adantr φ d N
102 100 101 adddirp1d φ d d + 1 N = d N + N
103 102 adantr φ d deg x G x d = d N d + 1 N = d N + N
104 57 98 103 3eqtr4rd φ d deg x G x d = d N d + 1 N = deg x G x d × f G
105 55 104 eqtr4d φ d deg x G x d = d N deg x G x d + 1 = d + 1 N
106 105 ex φ d deg x G x d = d N deg x G x d + 1 = d + 1 N
107 106 expcom d φ deg x G x d = d N deg x G x d + 1 = d + 1 N
108 107 a2d d φ deg x G x d = d N φ deg x G x d + 1 = d + 1 N
109 10 16 22 28 40 108 nnind M φ deg x G x M = M N
110 2 109 mpcom φ deg x G x M = M N