dgrcolem2

	Ref	Expression
Hypotheses	dgrco.1	$⊢ M = \deg (F)$
	dgrco.2	$⊢ N = \deg (G)$
	dgrco.3	$⊢ φ \to F \in Poly (S)$
	dgrco.4	$⊢ φ \to G \in Poly (S)$
	dgrco.5	$⊢ A = coeff (F)$
	dgrco.6	$⊢ φ \to D \in ℕ_{0}$
	dgrco.7	$⊢ φ \to M = D + 1$
	dgrco.8	$⊢ φ \to \forall f \in Poly (ℂ) (\deg (f) \leq D \to \deg (f \circ G) = \deg (f) \cdot N)$
Assertion	dgrcolem2	$⊢ φ \to \deg (F \circ G) = M \cdot N$

Proof

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

Metamath Proof Explorer

Theorem dgrcolem2

Proof