Theorem dgrco

Description: The degree of a composition of two polynomials is the product of the degrees. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	dgrco.1	⊢ 𝑀 = ( deg ‘ 𝐹 )
	dgrco.2	⊢ 𝑁 = ( deg ‘ 𝐺 )
	dgrco.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	dgrco.4	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
Assertion	dgrco	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		dgrco.1	⊢ 𝑀 = ( deg ‘ 𝐹 )
2		dgrco.2	⊢ 𝑁 = ( deg ‘ 𝐺 )
3		dgrco.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4		dgrco.4	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
5		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
6	5 3	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℂ ) )
7		dgrcl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
8	3 7	syl	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
9	1 8	eqeltrid	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
10		breq2	⊢ ( 𝑥 = 0 → ( ( deg ‘ 𝑓 ) ≤ 𝑥 ↔ ( deg ‘ 𝑓 ) ≤ 0 ) )
11	10	imbi1d	⊢ ( 𝑥 = 0 → ( ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ( ( deg ‘ 𝑓 ) ≤ 0 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
12	11	ralbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 0 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
13	12	imbi2d	⊢ ( 𝑥 = 0 → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 0 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ) )
14		breq2	⊢ ( 𝑥 = 𝑑 → ( ( deg ‘ 𝑓 ) ≤ 𝑥 ↔ ( deg ‘ 𝑓 ) ≤ 𝑑 ) )
15	14	imbi1d	⊢ ( 𝑥 = 𝑑 → ( ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
16	15	ralbidv	⊢ ( 𝑥 = 𝑑 → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
17	16	imbi2d	⊢ ( 𝑥 = 𝑑 → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ) )
18		breq2	⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( deg ‘ 𝑓 ) ≤ 𝑥 ↔ ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) ) )
19	18	imbi1d	⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
20	19	ralbidv	⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
21	20	imbi2d	⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ) )
22		breq2	⊢ ( 𝑥 = 𝑀 → ( ( deg ‘ 𝑓 ) ≤ 𝑥 ↔ ( deg ‘ 𝑓 ) ≤ 𝑀 ) )
23	22	imbi1d	⊢ ( 𝑥 = 𝑀 → ( ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ( ( deg ‘ 𝑓 ) ≤ 𝑀 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
24	23	ralbidv	⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑀 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
25	24	imbi2d	⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑥 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑀 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ) )
26		dgrcl	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
27	4 26	syl	⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℕ0 )
28	2 27	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
29	28	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
30	29	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → 𝑁 ∈ ℂ )
31	30	mul02d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( 0 · 𝑁 ) = 0 )
32		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( deg ‘ 𝑓 ) ≤ 0 )
33		dgrcl	⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) → ( deg ‘ 𝑓 ) ∈ ℕ0 )
34	33	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( deg ‘ 𝑓 ) ∈ ℕ0 )
35	34	nn0ge0d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → 0 ≤ ( deg ‘ 𝑓 ) )
36	34	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( deg ‘ 𝑓 ) ∈ ℝ )
37		0re	⊢ 0 ∈ ℝ
38		letri3	⊢ ( ( ( deg ‘ 𝑓 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( deg ‘ 𝑓 ) = 0 ↔ ( ( deg ‘ 𝑓 ) ≤ 0 ∧ 0 ≤ ( deg ‘ 𝑓 ) ) ) )
39	36 37 38	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( ( deg ‘ 𝑓 ) = 0 ↔ ( ( deg ‘ 𝑓 ) ≤ 0 ∧ 0 ≤ ( deg ‘ 𝑓 ) ) ) )
40	32 35 39	mpbir2and	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( deg ‘ 𝑓 ) = 0 )
41	40	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( ( deg ‘ 𝑓 ) · 𝑁 ) = ( 0 · 𝑁 ) )
42	31 41 40	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( ( deg ‘ 𝑓 ) · 𝑁 ) = ( deg ‘ 𝑓 ) )
43		fconstmpt	⊢ ( ℂ × { ( 𝑓 ‘ 0 ) } ) = ( 𝑦 ∈ ℂ ↦ ( 𝑓 ‘ 0 ) )
44		0dgrb	⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) → ( ( deg ‘ 𝑓 ) = 0 ↔ 𝑓 = ( ℂ × { ( 𝑓 ‘ 0 ) } ) ) )
45	44	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( ( deg ‘ 𝑓 ) = 0 ↔ 𝑓 = ( ℂ × { ( 𝑓 ‘ 0 ) } ) ) )
46	40 45	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → 𝑓 = ( ℂ × { ( 𝑓 ‘ 0 ) } ) )
47	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
48		plyf	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
49	47 48	syl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → 𝐺 : ℂ ⟶ ℂ )
50	49	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝐺 ‘ 𝑦 ) ∈ ℂ )
51	49	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → 𝐺 = ( 𝑦 ∈ ℂ ↦ ( 𝐺 ‘ 𝑦 ) ) )
52		fconstmpt	⊢ ( ℂ × { ( 𝑓 ‘ 0 ) } ) = ( 𝑥 ∈ ℂ ↦ ( 𝑓 ‘ 0 ) )
53	46 52	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → 𝑓 = ( 𝑥 ∈ ℂ ↦ ( 𝑓 ‘ 0 ) ) )
54		eqidd	⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 0 ) )
55	50 51 53 54	fmptco	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( 𝑓 ∘ 𝐺 ) = ( 𝑦 ∈ ℂ ↦ ( 𝑓 ‘ 0 ) ) )
56	43 46 55	3eqtr4a	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → 𝑓 = ( 𝑓 ∘ 𝐺 ) )
57	56	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( deg ‘ 𝑓 ) = ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) )
58	42 57	eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑓 ) ≤ 0 ) ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) )
59	58	expr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Poly ‘ ℂ ) ) → ( ( deg ‘ 𝑓 ) ≤ 0 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
60	59	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 0 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
61		fveq2	⊢ ( 𝑓 = 𝑔 → ( deg ‘ 𝑓 ) = ( deg ‘ 𝑔 ) )
62	61	breq1d	⊢ ( 𝑓 = 𝑔 → ( ( deg ‘ 𝑓 ) ≤ 𝑑 ↔ ( deg ‘ 𝑔 ) ≤ 𝑑 ) )
63		coeq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∘ 𝐺 ) = ( 𝑔 ∘ 𝐺 ) )
64	63	fveq2d	⊢ ( 𝑓 = 𝑔 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) )
65	61	oveq1d	⊢ ( 𝑓 = 𝑔 → ( ( deg ‘ 𝑓 ) · 𝑁 ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) )
66	64 65	eqeq12d	⊢ ( 𝑓 = 𝑔 → ( ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ↔ ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) )
67	62 66	imbi12d	⊢ ( 𝑓 = 𝑔 → ( ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) )
68	67	cbvralvw	⊢ ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) )
69	33	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( deg ‘ 𝑓 ) ∈ ℕ0 )
70	69	nn0red	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( deg ‘ 𝑓 ) ∈ ℝ )
71		nn0p1nn	⊢ ( 𝑑 ∈ ℕ0 → ( 𝑑 + 1 ) ∈ ℕ )
72	71	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( 𝑑 + 1 ) ∈ ℕ )
73	72	nnred	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( 𝑑 + 1 ) ∈ ℝ )
74	70 73	leloed	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) ↔ ( ( deg ‘ 𝑓 ) < ( 𝑑 + 1 ) ∨ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ) )
75		simplr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → 𝑑 ∈ ℕ0 )
76		nn0leltp1	⊢ ( ( ( deg ‘ 𝑓 ) ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) → ( ( deg ‘ 𝑓 ) ≤ 𝑑 ↔ ( deg ‘ 𝑓 ) < ( 𝑑 + 1 ) ) )
77	69 75 76	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( ( deg ‘ 𝑓 ) ≤ 𝑑 ↔ ( deg ‘ 𝑓 ) < ( 𝑑 + 1 ) ) )
78		fveq2	⊢ ( 𝑔 = 𝑓 → ( deg ‘ 𝑔 ) = ( deg ‘ 𝑓 ) )
79	78	breq1d	⊢ ( 𝑔 = 𝑓 → ( ( deg ‘ 𝑔 ) ≤ 𝑑 ↔ ( deg ‘ 𝑓 ) ≤ 𝑑 ) )
80		coeq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 ∘ 𝐺 ) = ( 𝑓 ∘ 𝐺 ) )
81	80	fveq2d	⊢ ( 𝑔 = 𝑓 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) )
82	78	oveq1d	⊢ ( 𝑔 = 𝑓 → ( ( deg ‘ 𝑔 ) · 𝑁 ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) )
83	81 82	eqeq12d	⊢ ( 𝑔 = 𝑓 → ( ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ↔ ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
84	79 83	imbi12d	⊢ ( 𝑔 = 𝑓 → ( ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ↔ ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
85	84	rspcva	⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) → ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
86	85	adantl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
87	77 86	sylbird	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( ( deg ‘ 𝑓 ) < ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
88		eqid	⊢ ( deg ‘ 𝑓 ) = ( deg ‘ 𝑓 )
89		simprll	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ) → 𝑓 ∈ ( Poly ‘ ℂ ) )
90	5 4	sselid	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ ℂ ) )
91	90	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
92		eqid	⊢ ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝑓 )
93		simplr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ) → 𝑑 ∈ ℕ0 )
94		simprr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ) → ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) )
95		simprlr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ) → ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) )
96		fveq2	⊢ ( 𝑔 = ℎ → ( deg ‘ 𝑔 ) = ( deg ‘ ℎ ) )
97	96	breq1d	⊢ ( 𝑔 = ℎ → ( ( deg ‘ 𝑔 ) ≤ 𝑑 ↔ ( deg ‘ ℎ ) ≤ 𝑑 ) )
98		coeq1	⊢ ( 𝑔 = ℎ → ( 𝑔 ∘ 𝐺 ) = ( ℎ ∘ 𝐺 ) )
99	98	fveq2d	⊢ ( 𝑔 = ℎ → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( deg ‘ ( ℎ ∘ 𝐺 ) ) )
100	96	oveq1d	⊢ ( 𝑔 = ℎ → ( ( deg ‘ 𝑔 ) · 𝑁 ) = ( ( deg ‘ ℎ ) · 𝑁 ) )
101	99 100	eqeq12d	⊢ ( 𝑔 = ℎ → ( ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ↔ ( deg ‘ ( ℎ ∘ 𝐺 ) ) = ( ( deg ‘ ℎ ) · 𝑁 ) ) )
102	97 101	imbi12d	⊢ ( 𝑔 = ℎ → ( ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ↔ ( ( deg ‘ ℎ ) ≤ 𝑑 → ( deg ‘ ( ℎ ∘ 𝐺 ) ) = ( ( deg ‘ ℎ ) · 𝑁 ) ) ) )
103	102	cbvralvw	⊢ ( ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ↔ ∀ ℎ ∈ ( Poly ‘ ℂ ) ( ( deg ‘ ℎ ) ≤ 𝑑 → ( deg ‘ ( ℎ ∘ 𝐺 ) ) = ( ( deg ‘ ℎ ) · 𝑁 ) ) )
104	95 103	sylib	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ) → ∀ ℎ ∈ ( Poly ‘ ℂ ) ( ( deg ‘ ℎ ) ≤ 𝑑 → ( deg ‘ ( ℎ ∘ 𝐺 ) ) = ( ( deg ‘ ℎ ) · 𝑁 ) ) )
105	88 2 89 91 92 93 94 104	dgrcolem2	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) )
106	105	expr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
107	87 106	jaod	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( ( ( deg ‘ 𝑓 ) < ( 𝑑 + 1 ) ∨ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
108	74 107	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) ) ) → ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
109	108	expr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ ℂ ) ) → ( ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) → ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
110	109	ralrimdva	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑔 ) ≤ 𝑑 → ( deg ‘ ( 𝑔 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) · 𝑁 ) ) → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
111	68 110	biimtrid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
112	111	expcom	⊢ ( 𝑑 ∈ ℕ0 → ( 𝜑 → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ) )
113	112	a2d	⊢ ( 𝑑 ∈ ℕ0 → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑑 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) → ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ ( 𝑑 + 1 ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) ) )
114	13 17 21 25 60 113	nn0ind	⊢ ( 𝑀 ∈ ℕ0 → ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑀 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ) )
115	9 114	mpcom	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑀 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
116	9	nn0red	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
117	116	leidd	⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
118		fveq2	⊢ ( 𝑓 = 𝐹 → ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) )
119	118 1	eqtr4di	⊢ ( 𝑓 = 𝐹 → ( deg ‘ 𝑓 ) = 𝑀 )
120	119	breq1d	⊢ ( 𝑓 = 𝐹 → ( ( deg ‘ 𝑓 ) ≤ 𝑀 ↔ 𝑀 ≤ 𝑀 ) )
121		coeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
122	121	fveq2d	⊢ ( 𝑓 = 𝐹 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) )
123	119	oveq1d	⊢ ( 𝑓 = 𝐹 → ( ( deg ‘ 𝑓 ) · 𝑁 ) = ( 𝑀 · 𝑁 ) )
124	122 123	eqeq12d	⊢ ( 𝑓 = 𝐹 → ( ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ↔ ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) ) )
125	120 124	imbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( deg ‘ 𝑓 ) ≤ 𝑀 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ( 𝑀 ≤ 𝑀 → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) ) ) )
126	125	rspcv	⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝑀 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) → ( 𝑀 ≤ 𝑀 → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) ) ) )
127	6 115 117 126	syl3c	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) )