Metamath Proof Explorer

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 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) )