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 
|- ( ph -> M e. NN )
dgrcolem1.3 
|- ( ph -> N e. NN )
dgrcolem1.4 
|- ( ph -> G e. ( Poly ` S ) )
Assertion dgrcolem1 
|- ( ph -> ( deg ` ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) = ( M x. N ) )

Proof

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