This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dgrcolem2

Description: Lemma for dgrco . (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses dgrco.1 
|- M = ( deg ` F )
dgrco.2 
|- N = ( deg ` G )
dgrco.3 
|- ( ph -> F e. ( Poly ` S ) )
dgrco.4 
|- ( ph -> G e. ( Poly ` S ) )
dgrco.5 
|- A = ( coeff ` F )
dgrco.6 
|- ( ph -> D e. NN0 )
dgrco.7 
|- ( ph -> M = ( D + 1 ) )
dgrco.8 
|- ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ D -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
Assertion dgrcolem2 
|- ( ph -> ( deg ` ( F o. G ) ) = ( M x. N ) )

Proof

Step Hyp Ref Expression
1 dgrco.1 
 |-  M = ( deg ` F )
2 dgrco.2 
 |-  N = ( deg ` G )
3 dgrco.3 
 |-  ( ph -> F e. ( Poly ` S ) )
4 dgrco.4 
 |-  ( ph -> G e. ( Poly ` S ) )
5 dgrco.5 
 |-  A = ( coeff ` F )
6 dgrco.6 
 |-  ( ph -> D e. NN0 )
7 dgrco.7 
 |-  ( ph -> M = ( D + 1 ) )
8 dgrco.8 
 |-  ( ph -> A. f e. ( Poly ` CC ) ( ( deg ` f ) <_ D -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) )
9 plyf 
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
10 4 9 syl 
 |-  ( ph -> G : CC --> CC )
11 10 ffvelcdmda 
 |-  ( ( ph /\ x e. CC ) -> ( G ` x ) e. CC )
12 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
13 3 12 syl 
 |-  ( ph -> F : CC --> CC )
14 13 ffvelcdmda 
 |-  ( ( ph /\ ( G ` x ) e. CC ) -> ( F ` ( G ` x ) ) e. CC )
15 11 14 syldan 
 |-  ( ( ph /\ x e. CC ) -> ( F ` ( G ` x ) ) e. CC )
16 5 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
17 3 16 syl 
 |-  ( ph -> A : NN0 --> CC )
18 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
19 3 18 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
20 1 19 eqeltrid 
 |-  ( ph -> M e. NN0 )
21 17 20 ffvelcdmd 
 |-  ( ph -> ( A ` M ) e. CC )
22 21 adantr 
 |-  ( ( ph /\ x e. CC ) -> ( A ` M ) e. CC )
23 20 adantr 
 |-  ( ( ph /\ x e. CC ) -> M e. NN0 )
24 11 23 expcld 
 |-  ( ( ph /\ x e. CC ) -> ( ( G ` x ) ^ M ) e. CC )
25 22 24 mulcld 
 |-  ( ( ph /\ x e. CC ) -> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) e. CC )
26 15 25 npcand 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) + ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) = ( F ` ( G ` x ) ) )
27 26 mpteq2dva 
 |-  ( ph -> ( x e. CC |-> ( ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) + ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) = ( x e. CC |-> ( F ` ( G ` x ) ) ) )
28 cnex 
 |-  CC e. _V
29 28 a1i 
 |-  ( ph -> CC e. _V )
30 15 25 subcld 
 |-  ( ( ph /\ x e. CC ) -> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) e. CC )
31 eqidd 
 |-  ( ph -> ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) = ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
32 eqidd 
 |-  ( ph -> ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) = ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) )
33 29 30 25 31 32 offval2 
 |-  ( ph -> ( ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) oF + ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) = ( x e. CC |-> ( ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) + ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
34 10 feqmptd 
 |-  ( ph -> G = ( x e. CC |-> ( G ` x ) ) )
35 13 feqmptd 
 |-  ( ph -> F = ( y e. CC |-> ( F ` y ) ) )
36 fveq2 
 |-  ( y = ( G ` x ) -> ( F ` y ) = ( F ` ( G ` x ) ) )
37 11 34 35 36 fmptco 
 |-  ( ph -> ( F o. G ) = ( x e. CC |-> ( F ` ( G ` x ) ) ) )
38 27 33 37 3eqtr4rd 
 |-  ( ph -> ( F o. G ) = ( ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) oF + ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
39 38 fveq2d 
 |-  ( ph -> ( deg ` ( F o. G ) ) = ( deg ` ( ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) oF + ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) )
40 39 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( F o. G ) ) = ( deg ` ( ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) oF + ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) )
41 29 15 25 37 32 offval2 
 |-  ( ph -> ( ( F o. G ) oF - ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) = ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
42 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
43 42 3 sselid 
 |-  ( ph -> F e. ( Poly ` CC ) )
44 42 4 sselid 
 |-  ( ph -> G e. ( Poly ` CC ) )
45 addcl 
 |-  ( ( z e. CC /\ w e. CC ) -> ( z + w ) e. CC )
46 45 adantl 
 |-  ( ( ph /\ ( z e. CC /\ w e. CC ) ) -> ( z + w ) e. CC )
47 mulcl 
 |-  ( ( z e. CC /\ w e. CC ) -> ( z x. w ) e. CC )
48 47 adantl 
 |-  ( ( ph /\ ( z e. CC /\ w e. CC ) ) -> ( z x. w ) e. CC )
49 43 44 46 48 plyco 
 |-  ( ph -> ( F o. G ) e. ( Poly ` CC ) )
50 eqidd 
 |-  ( ph -> ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) = ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) )
51 oveq1 
 |-  ( y = ( G ` x ) -> ( y ^ M ) = ( ( G ` x ) ^ M ) )
52 51 oveq2d 
 |-  ( y = ( G ` x ) -> ( ( A ` M ) x. ( y ^ M ) ) = ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) )
53 11 34 50 52 fmptco 
 |-  ( ph -> ( ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) o. G ) = ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) )
54 ssidd 
 |-  ( ph -> CC C_ CC )
55 eqid 
 |-  ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) = ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) )
56 55 ply1term 
 |-  ( ( CC C_ CC /\ ( A ` M ) e. CC /\ M e. NN0 ) -> ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) e. ( Poly ` CC ) )
57 54 21 20 56 syl3anc 
 |-  ( ph -> ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) e. ( Poly ` CC ) )
58 57 44 46 48 plyco 
 |-  ( ph -> ( ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) o. G ) e. ( Poly ` CC ) )
59 53 58 eqeltrrd 
 |-  ( ph -> ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) e. ( Poly ` CC ) )
60 plysubcl 
 |-  ( ( ( F o. G ) e. ( Poly ` CC ) /\ ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) e. ( Poly ` CC ) ) -> ( ( F o. G ) oF - ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) e. ( Poly ` CC ) )
61 49 59 60 syl2anc 
 |-  ( ph -> ( ( F o. G ) oF - ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) e. ( Poly ` CC ) )
62 41 61 eqeltrrd 
 |-  ( ph -> ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) e. ( Poly ` CC ) )
63 62 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) e. ( Poly ` CC ) )
64 59 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) e. ( Poly ` CC ) )
65 nn0p1nn 
 |-  ( D e. NN0 -> ( D + 1 ) e. NN )
66 6 65 syl 
 |-  ( ph -> ( D + 1 ) e. NN )
67 7 66 eqeltrd 
 |-  ( ph -> M e. NN )
68 67 nngt0d 
 |-  ( ph -> 0 < M )
69 fveq2 
 |-  ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = 0p -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) = ( deg ` 0p ) )
70 dgr0 
 |-  ( deg ` 0p ) = 0
71 69 70 eqtrdi 
 |-  ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = 0p -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) = 0 )
72 71 breq1d 
 |-  ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = 0p -> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M <-> 0 < M ) )
73 68 72 syl5ibrcom 
 |-  ( ph -> ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = 0p -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M ) )
74 idd 
 |-  ( ph -> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M ) )
75 eqid 
 |-  ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) )
76 1 75 dgrsub 
 |-  ( ( F e. ( Poly ` CC ) /\ ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) e. ( Poly ` CC ) ) -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ if ( M <_ ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , M ) )
77 43 57 76 syl2anc 
 |-  ( ph -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ if ( M <_ ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , M ) )
78 67 nnne0d 
 |-  ( ph -> M =/= 0 )
79 1 5 dgreq0 
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` M ) = 0 ) )
80 3 79 syl 
 |-  ( ph -> ( F = 0p <-> ( A ` M ) = 0 ) )
81 fveq2 
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
82 81 70 eqtrdi 
 |-  ( F = 0p -> ( deg ` F ) = 0 )
83 1 82 eqtrid 
 |-  ( F = 0p -> M = 0 )
84 80 83 biimtrrdi 
 |-  ( ph -> ( ( A ` M ) = 0 -> M = 0 ) )
85 84 necon3d 
 |-  ( ph -> ( M =/= 0 -> ( A ` M ) =/= 0 ) )
86 78 85 mpd 
 |-  ( ph -> ( A ` M ) =/= 0 )
87 55 dgr1term 
 |-  ( ( ( A ` M ) e. CC /\ ( A ` M ) =/= 0 /\ M e. NN0 ) -> ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = M )
88 21 86 20 87 syl3anc 
 |-  ( ph -> ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = M )
89 88 ifeq1d 
 |-  ( ph -> if ( M <_ ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , M ) = if ( M <_ ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , M , M ) )
90 ifid 
 |-  if ( M <_ ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , M , M ) = M
91 89 90 eqtrdi 
 |-  ( ph -> if ( M <_ ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , ( deg ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) , M ) = M )
92 77 91 breqtrd 
 |-  ( ph -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ M )
93 eqid 
 |-  ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) )
94 5 93 coesub 
 |-  ( ( F e. ( Poly ` CC ) /\ ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) e. ( Poly ` CC ) ) -> ( coeff ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) = ( A oF - ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) )
95 43 57 94 syl2anc 
 |-  ( ph -> ( coeff ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) = ( A oF - ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) )
96 95 fveq1d 
 |-  ( ph -> ( ( coeff ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) ` M ) = ( ( A oF - ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) ` M ) )
97 17 ffnd 
 |-  ( ph -> A Fn NN0 )
98 93 coef3 
 |-  ( ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) e. ( Poly ` CC ) -> ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) : NN0 --> CC )
99 57 98 syl 
 |-  ( ph -> ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) : NN0 --> CC )
100 99 ffnd 
 |-  ( ph -> ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) Fn NN0 )
101 nn0ex 
 |-  NN0 e. _V
102 101 a1i 
 |-  ( ph -> NN0 e. _V )
103 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
104 eqidd 
 |-  ( ( ph /\ M e. NN0 ) -> ( A ` M ) = ( A ` M ) )
105 55 coe1term 
 |-  ( ( ( A ` M ) e. CC /\ M e. NN0 /\ M e. NN0 ) -> ( ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ` M ) = if ( M = M , ( A ` M ) , 0 ) )
106 21 20 20 105 syl3anc 
 |-  ( ph -> ( ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ` M ) = if ( M = M , ( A ` M ) , 0 ) )
107 eqid 
 |-  M = M
108 107 iftruei 
 |-  if ( M = M , ( A ` M ) , 0 ) = ( A ` M )
109 106 108 eqtrdi 
 |-  ( ph -> ( ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ` M ) = ( A ` M ) )
110 109 adantr 
 |-  ( ( ph /\ M e. NN0 ) -> ( ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ` M ) = ( A ` M ) )
111 97 100 102 102 103 104 110 ofval 
 |-  ( ( ph /\ M e. NN0 ) -> ( ( A oF - ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) ` M ) = ( ( A ` M ) - ( A ` M ) ) )
112 20 111 mpdan 
 |-  ( ph -> ( ( A oF - ( coeff ` ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) ` M ) = ( ( A ` M ) - ( A ` M ) ) )
113 21 subidd 
 |-  ( ph -> ( ( A ` M ) - ( A ` M ) ) = 0 )
114 96 112 113 3eqtrd 
 |-  ( ph -> ( ( coeff ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) ` M ) = 0 )
115 plysubcl 
 |-  ( ( F e. ( Poly ` CC ) /\ ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) e. ( Poly ` CC ) ) -> ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) e. ( Poly ` CC ) )
116 43 57 115 syl2anc 
 |-  ( ph -> ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) e. ( Poly ` CC ) )
117 eqid 
 |-  ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) = ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) )
118 eqid 
 |-  ( coeff ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) = ( coeff ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) )
119 117 118 dgrlt 
 |-  ( ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) e. ( Poly ` CC ) /\ M e. NN0 ) -> ( ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = 0p \/ ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M ) <-> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ M /\ ( ( coeff ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) ` M ) = 0 ) ) )
120 116 20 119 syl2anc 
 |-  ( ph -> ( ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = 0p \/ ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M ) <-> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ M /\ ( ( coeff ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) ` M ) = 0 ) ) )
121 92 114 120 mpbir2and 
 |-  ( ph -> ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = 0p \/ ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M ) )
122 73 74 121 mpjaod 
 |-  ( ph -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M )
123 122 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M )
124 dgrcl 
 |-  ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) e. ( Poly ` CC ) -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) e. NN0 )
125 116 124 syl 
 |-  ( ph -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) e. NN0 )
126 125 nn0red 
 |-  ( ph -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) e. RR )
127 126 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) e. RR )
128 20 nn0red 
 |-  ( ph -> M e. RR )
129 128 adantr 
 |-  ( ( ph /\ N e. NN ) -> M e. RR )
130 nnre 
 |-  ( N e. NN -> N e. RR )
131 130 adantl 
 |-  ( ( ph /\ N e. NN ) -> N e. RR )
132 nngt0 
 |-  ( N e. NN -> 0 < N )
133 132 adantl 
 |-  ( ( ph /\ N e. NN ) -> 0 < N )
134 ltmul1 
 |-  ( ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) e. RR /\ M e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M <-> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) < ( M x. N ) ) )
135 127 129 131 133 134 syl112anc 
 |-  ( ( ph /\ N e. NN ) -> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < M <-> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) < ( M x. N ) ) )
136 123 135 mpbid 
 |-  ( ( ph /\ N e. NN ) -> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) < ( M x. N ) )
137 13 ffvelcdmda 
 |-  ( ( ph /\ y e. CC ) -> ( F ` y ) e. CC )
138 21 adantr 
 |-  ( ( ph /\ y e. CC ) -> ( A ` M ) e. CC )
139 id 
 |-  ( y e. CC -> y e. CC )
140 expcl 
 |-  ( ( y e. CC /\ M e. NN0 ) -> ( y ^ M ) e. CC )
141 139 20 140 syl2anr 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ M ) e. CC )
142 138 141 mulcld 
 |-  ( ( ph /\ y e. CC ) -> ( ( A ` M ) x. ( y ^ M ) ) e. CC )
143 29 137 142 35 50 offval2 
 |-  ( ph -> ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) = ( y e. CC |-> ( ( F ` y ) - ( ( A ` M ) x. ( y ^ M ) ) ) ) )
144 36 52 oveq12d 
 |-  ( y = ( G ` x ) -> ( ( F ` y ) - ( ( A ` M ) x. ( y ^ M ) ) ) = ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) )
145 11 34 143 144 fmptco 
 |-  ( ph -> ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) o. G ) = ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
146 145 fveq2d 
 |-  ( ph -> ( deg ` ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) o. G ) ) = ( deg ` ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) )
147 122 7 breqtrd 
 |-  ( ph -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < ( D + 1 ) )
148 nn0leltp1 
 |-  ( ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) e. NN0 /\ D e. NN0 ) -> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ D <-> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < ( D + 1 ) ) )
149 125 6 148 syl2anc 
 |-  ( ph -> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ D <-> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) < ( D + 1 ) ) )
150 147 149 mpbird 
 |-  ( ph -> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ D )
151 fveq2 
 |-  ( f = ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) -> ( deg ` f ) = ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) )
152 151 breq1d 
 |-  ( f = ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) -> ( ( deg ` f ) <_ D <-> ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ D ) )
153 coeq1 
 |-  ( f = ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) -> ( f o. G ) = ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) o. G ) )
154 153 fveq2d 
 |-  ( f = ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) -> ( deg ` ( f o. G ) ) = ( deg ` ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) o. G ) ) )
155 151 oveq1d 
 |-  ( f = ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) -> ( ( deg ` f ) x. N ) = ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) )
156 154 155 eqeq12d 
 |-  ( f = ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) -> ( ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) <-> ( deg ` ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) o. G ) ) = ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) ) )
157 152 156 imbi12d 
 |-  ( f = ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) -> ( ( ( deg ` f ) <_ D -> ( deg ` ( f o. G ) ) = ( ( deg ` f ) x. N ) ) <-> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ D -> ( deg ` ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) o. G ) ) = ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) ) ) )
158 157 8 116 rspcdva 
 |-  ( ph -> ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) <_ D -> ( deg ` ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) o. G ) ) = ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) ) )
159 150 158 mpd 
 |-  ( ph -> ( deg ` ( ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) o. G ) ) = ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) )
160 146 159 eqtr3d 
 |-  ( ph -> ( deg ` ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) = ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) )
161 160 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) = ( ( deg ` ( F oF - ( y e. CC |-> ( ( A ` M ) x. ( y ^ M ) ) ) ) ) x. N ) )
162 fconstmpt 
 |-  ( CC X. { ( A ` M ) } ) = ( x e. CC |-> ( A ` M ) )
163 162 a1i 
 |-  ( ph -> ( CC X. { ( A ` M ) } ) = ( x e. CC |-> ( A ` M ) ) )
164 eqidd 
 |-  ( ph -> ( x e. CC |-> ( ( G ` x ) ^ M ) ) = ( x e. CC |-> ( ( G ` x ) ^ M ) ) )
165 29 22 24 163 164 offval2 
 |-  ( ph -> ( ( CC X. { ( A ` M ) } ) oF x. ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) = ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) )
166 165 fveq2d 
 |-  ( ph -> ( deg ` ( ( CC X. { ( A ` M ) } ) oF x. ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) ) = ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
167 eqidd 
 |-  ( ph -> ( y e. CC |-> ( y ^ M ) ) = ( y e. CC |-> ( y ^ M ) ) )
168 11 34 167 51 fmptco 
 |-  ( ph -> ( ( y e. CC |-> ( y ^ M ) ) o. G ) = ( x e. CC |-> ( ( G ` x ) ^ M ) ) )
169 1cnd 
 |-  ( ph -> 1 e. CC )
170 plypow 
 |-  ( ( CC C_ CC /\ 1 e. CC /\ M e. NN0 ) -> ( y e. CC |-> ( y ^ M ) ) e. ( Poly ` CC ) )
171 54 169 20 170 syl3anc 
 |-  ( ph -> ( y e. CC |-> ( y ^ M ) ) e. ( Poly ` CC ) )
172 171 44 46 48 plyco 
 |-  ( ph -> ( ( y e. CC |-> ( y ^ M ) ) o. G ) e. ( Poly ` CC ) )
173 168 172 eqeltrrd 
 |-  ( ph -> ( x e. CC |-> ( ( G ` x ) ^ M ) ) e. ( Poly ` CC ) )
174 dgrmulc 
 |-  ( ( ( A ` M ) e. CC /\ ( A ` M ) =/= 0 /\ ( x e. CC |-> ( ( G ` x ) ^ M ) ) e. ( Poly ` CC ) ) -> ( deg ` ( ( CC X. { ( A ` M ) } ) oF x. ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) ) = ( deg ` ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) )
175 21 86 173 174 syl3anc 
 |-  ( ph -> ( deg ` ( ( CC X. { ( A ` M ) } ) oF x. ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) ) = ( deg ` ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) )
176 166 175 eqtr3d 
 |-  ( ph -> ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) = ( deg ` ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) )
177 176 adantr 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) = ( deg ` ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) )
178 67 adantr 
 |-  ( ( ph /\ N e. NN ) -> M e. NN )
179 simpr 
 |-  ( ( ph /\ N e. NN ) -> N e. NN )
180 4 adantr 
 |-  ( ( ph /\ N e. NN ) -> G e. ( Poly ` S ) )
181 2 178 179 180 dgrcolem1 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( x e. CC |-> ( ( G ` x ) ^ M ) ) ) = ( M x. N ) )
182 177 181 eqtrd 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) = ( M x. N ) )
183 136 161 182 3brtr4d 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) < ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
184 eqid 
 |-  ( deg ` ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) = ( deg ` ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
185 eqid 
 |-  ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) = ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) )
186 184 185 dgradd2 
 |-  ( ( ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) e. ( Poly ` CC ) /\ ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) e. ( Poly ` CC ) /\ ( deg ` ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) < ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) -> ( deg ` ( ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) oF + ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) = ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
187 63 64 183 186 syl3anc 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( ( x e. CC |-> ( ( F ` ( G ` x ) ) - ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) oF + ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) ) = ( deg ` ( x e. CC |-> ( ( A ` M ) x. ( ( G ` x ) ^ M ) ) ) ) )
188 40 187 182 3eqtrd 
 |-  ( ( ph /\ N e. NN ) -> ( deg ` ( F o. G ) ) = ( M x. N ) )
189 0cn 
 |-  0 e. CC
190 ffvelcdm 
 |-  ( ( G : CC --> CC /\ 0 e. CC ) -> ( G ` 0 ) e. CC )
191 10 189 190 sylancl 
 |-  ( ph -> ( G ` 0 ) e. CC )
192 13 191 ffvelcdmd 
 |-  ( ph -> ( F ` ( G ` 0 ) ) e. CC )
193 0dgr 
 |-  ( ( F ` ( G ` 0 ) ) e. CC -> ( deg ` ( CC X. { ( F ` ( G ` 0 ) ) } ) ) = 0 )
194 192 193 syl 
 |-  ( ph -> ( deg ` ( CC X. { ( F ` ( G ` 0 ) ) } ) ) = 0 )
195 20 nn0cnd 
 |-  ( ph -> M e. CC )
196 195 mul01d 
 |-  ( ph -> ( M x. 0 ) = 0 )
197 194 196 eqtr4d 
 |-  ( ph -> ( deg ` ( CC X. { ( F ` ( G ` 0 ) ) } ) ) = ( M x. 0 ) )
198 197 adantr 
 |-  ( ( ph /\ N = 0 ) -> ( deg ` ( CC X. { ( F ` ( G ` 0 ) ) } ) ) = ( M x. 0 ) )
199 191 ad2antrr 
 |-  ( ( ( ph /\ N = 0 ) /\ x e. CC ) -> ( G ` 0 ) e. CC )
200 simpr 
 |-  ( ( ph /\ N = 0 ) -> N = 0 )
201 2 200 eqtr3id 
 |-  ( ( ph /\ N = 0 ) -> ( deg ` G ) = 0 )
202 0dgrb 
 |-  ( G e. ( Poly ` S ) -> ( ( deg ` G ) = 0 <-> G = ( CC X. { ( G ` 0 ) } ) ) )
203 4 202 syl 
 |-  ( ph -> ( ( deg ` G ) = 0 <-> G = ( CC X. { ( G ` 0 ) } ) ) )
204 203 adantr 
 |-  ( ( ph /\ N = 0 ) -> ( ( deg ` G ) = 0 <-> G = ( CC X. { ( G ` 0 ) } ) ) )
205 201 204 mpbid 
 |-  ( ( ph /\ N = 0 ) -> G = ( CC X. { ( G ` 0 ) } ) )
206 fconstmpt 
 |-  ( CC X. { ( G ` 0 ) } ) = ( x e. CC |-> ( G ` 0 ) )
207 205 206 eqtrdi 
 |-  ( ( ph /\ N = 0 ) -> G = ( x e. CC |-> ( G ` 0 ) ) )
208 35 adantr 
 |-  ( ( ph /\ N = 0 ) -> F = ( y e. CC |-> ( F ` y ) ) )
209 fveq2 
 |-  ( y = ( G ` 0 ) -> ( F ` y ) = ( F ` ( G ` 0 ) ) )
210 199 207 208 209 fmptco 
 |-  ( ( ph /\ N = 0 ) -> ( F o. G ) = ( x e. CC |-> ( F ` ( G ` 0 ) ) ) )
211 fconstmpt 
 |-  ( CC X. { ( F ` ( G ` 0 ) ) } ) = ( x e. CC |-> ( F ` ( G ` 0 ) ) )
212 210 211 eqtr4di 
 |-  ( ( ph /\ N = 0 ) -> ( F o. G ) = ( CC X. { ( F ` ( G ` 0 ) ) } ) )
213 212 fveq2d 
 |-  ( ( ph /\ N = 0 ) -> ( deg ` ( F o. G ) ) = ( deg ` ( CC X. { ( F ` ( G ` 0 ) ) } ) ) )
214 200 oveq2d 
 |-  ( ( ph /\ N = 0 ) -> ( M x. N ) = ( M x. 0 ) )
215 198 213 214 3eqtr4d 
 |-  ( ( ph /\ N = 0 ) -> ( deg ` ( F o. G ) ) = ( M x. N ) )
216 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
217 4 216 syl 
 |-  ( ph -> ( deg ` G ) e. NN0 )
218 2 217 eqeltrid 
 |-  ( ph -> N e. NN0 )
219 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
220 218 219 sylib 
 |-  ( ph -> ( N e. NN \/ N = 0 ) )
221 188 215 220 mpjaodan 
 |-  ( ph -> ( deg ` ( F o. G ) ) = ( M x. N ) )