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	ffvelrnda	|- ( ( 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	ffvelrnda	|- ( ( 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	ffvelrnd	|- ( 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	sseldi	|- ( ph -> F e. ( Poly ` CC ) )
44	42 4	sseldi	|- ( 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	syl5eq	|- ( F = 0p -> M = 0 )
84	80 83	syl6bir	|- ( 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	ffvelrnda	|- ( ( 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		ffvelrn	|- ( ( G : CC --> CC /\ 0 e. CC ) -> ( G ` 0 ) e. CC )
191	10 189 190	sylancl	|- ( ph -> ( G ` 0 ) e. CC )
192	13 191	ffvelrnd	|- ( 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 ) )