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

Metamath Proof Explorer

Theorem dgrcolem1

Description: The degree of a composition of a monomial with a polynomial. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses dgrcolem1.1 ⊢ 𝑁 = ( deg ‘ 𝐺 )
dgrcolem1.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
dgrcolem1.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dgrcolem1.4 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
Assertion dgrcolem1 ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝑀 · 𝑁 ) )

Proof

Step Hyp Ref Expression
1 dgrcolem1.1 ⊢ 𝑁 = ( deg ‘ 𝐺 )
2 dgrcolem1.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 dgrcolem1.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 dgrcolem1.4 ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
5 oveq2 ⊢ ( 𝑦 = 1 → ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) = ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) )
6 5 mpteq2dv ⊢ ( 𝑦 = 1 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) )
7 6 fveq2d ⊢ ( 𝑦 = 1 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) ) )
8 oveq1 ⊢ ( 𝑦 = 1 → ( 𝑦 · 𝑁 ) = ( 1 · 𝑁 ) )
9 7 8 eqeq12d ⊢ ( 𝑦 = 1 → ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( 𝑦 · 𝑁 ) ↔ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) ) = ( 1 · 𝑁 ) ) )
10 9 imbi2d ⊢ ( 𝑦 = 1 → ( ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( 𝑦 · 𝑁 ) ) ↔ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) ) = ( 1 · 𝑁 ) ) ) )
11 oveq2 ⊢ ( 𝑦 = 𝑑 → ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) = ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) )
12 11 mpteq2dv ⊢ ( 𝑦 = 𝑑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) )
13 12 fveq2d ⊢ ( 𝑦 = 𝑑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) )
14 oveq1 ⊢ ( 𝑦 = 𝑑 → ( 𝑦 · 𝑁 ) = ( 𝑑 · 𝑁 ) )
15 13 14 eqeq12d ⊢ ( 𝑦 = 𝑑 → ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( 𝑦 · 𝑁 ) ↔ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) )
16 15 imbi2d ⊢ ( 𝑦 = 𝑑 → ( ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( 𝑦 · 𝑁 ) ) ↔ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) ) )
17 oveq2 ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) = ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) )
18 17 mpteq2dv ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) )
19 18 fveq2d ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) )
20 oveq1 ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( 𝑦 · 𝑁 ) = ( ( 𝑑 + 1 ) · 𝑁 ) )
21 19 20 eqeq12d ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( 𝑦 · 𝑁 ) ↔ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) = ( ( 𝑑 + 1 ) · 𝑁 ) ) )
22 21 imbi2d ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( 𝑦 · 𝑁 ) ) ↔ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) = ( ( 𝑑 + 1 ) · 𝑁 ) ) ) )
23 oveq2 ⊢ ( 𝑦 = 𝑀 → ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) = ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) )
24 23 mpteq2dv ⊢ ( 𝑦 = 𝑀 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) )
25 24 fveq2d ⊢ ( 𝑦 = 𝑀 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
26 oveq1 ⊢ ( 𝑦 = 𝑀 → ( 𝑦 · 𝑁 ) = ( 𝑀 · 𝑁 ) )
27 25 26 eqeq12d ⊢ ( 𝑦 = 𝑀 → ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( 𝑦 · 𝑁 ) ↔ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝑀 · 𝑁 ) ) )
28 27 imbi2d ⊢ ( 𝑦 = 𝑀 → ( ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑦 ) ) ) = ( 𝑦 · 𝑁 ) ) ↔ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝑀 · 𝑁 ) ) ) )
29 plyf ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
30 4 29 syl ⊢ ( 𝜑 → 𝐺 : ℂ ⟶ ℂ )
31 30 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
32 31 exp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) = ( 𝐺 ‘ 𝑥 ) )
33 32 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐺 ‘ 𝑥 ) ) )
34 30 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝐺 ‘ 𝑥 ) ) )
35 33 34 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) = 𝐺 )
36 35 fveq2d ⊢ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) ) = ( deg ‘ 𝐺 ) )
37 36 1 eqtr4di ⊢ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) ) = 𝑁 )
38 3 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
39 38 mullidd ⊢ ( 𝜑 → ( 1 · 𝑁 ) = 𝑁 )
40 37 39 eqtr4d ⊢ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 1 ) ) ) = ( 1 · 𝑁 ) )
41 31 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
42 nnnn0 ⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℕ0 )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝑑 ∈ ℕ0 )
44 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → 𝑑 ∈ ℕ0 )
45 41 44 expp1d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) = ( ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) · ( 𝐺 ‘ 𝑥 ) ) )
46 45 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
47 cnex ⊢ ℂ ∈ V
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ℂ ∈ V )
49 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ∈ V )
50 eqidd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) )
51 34 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝐺 ‘ 𝑥 ) ) )
52 48 49 41 50 51 offval2 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∘f · 𝐺 ) = ( 𝑥 ∈ ℂ ↦ ( ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
53 46 52 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) = ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∘f · 𝐺 ) )
54 53 fveq2d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) = ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∘f · 𝐺 ) ) )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) = ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∘f · 𝐺 ) ) )
56 oveq1 ⊢ ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) → ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) + 𝑁 ) = ( ( 𝑑 · 𝑁 ) + 𝑁 ) )
57 56 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) + 𝑁 ) = ( ( 𝑑 · 𝑁 ) + 𝑁 ) )
58 eqidd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑑 ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑑 ) ) )
59 oveq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( 𝑦 ↑ 𝑑 ) = ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) )
60 41 51 58 59 fmptco ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑑 ) ) ∘ 𝐺 ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) )
61 ssidd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ℂ ⊆ ℂ )
62 1cnd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 1 ∈ ℂ )
63 plypow ⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ∧ 𝑑 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑑 ) ) ∈ ( Poly ‘ ℂ ) )
64 61 62 43 63 syl3anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑑 ) ) ∈ ( Poly ‘ ℂ ) )
65 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
66 4 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
67 65 66 sselid ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
68 addcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑧 + 𝑤 ) ∈ ℂ )
69 68 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( 𝑧 + 𝑤 ) ∈ ℂ )
70 mulcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑧 · 𝑤 ) ∈ ℂ )
71 70 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( 𝑧 · 𝑤 ) ∈ ℂ )
72 64 67 69 71 plyco ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑑 ) ) ∘ 𝐺 ) ∈ ( Poly ‘ ℂ ) )
73 60 72 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∈ ( Poly ‘ ℂ ) )
74 73 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∈ ( Poly ‘ ℂ ) )
75 simpr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) )
76 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝑑 ∈ ℕ )
77 3 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝑁 ∈ ℕ )
78 76 77 nnmulcld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( 𝑑 · 𝑁 ) ∈ ℕ )
79 78 nnne0d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( 𝑑 · 𝑁 ) ≠ 0 )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( 𝑑 · 𝑁 ) ≠ 0 )
81 75 80 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) ≠ 0 )
82 fveq2 ⊢ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) = 0𝑝 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( deg ‘ 0𝑝 ) )
83 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
84 82 83 eqtrdi ⊢ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) = 0𝑝 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = 0 )
85 84 necon3i ⊢ ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) ≠ 0 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ≠ 0𝑝 )
86 81 85 syl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ≠ 0𝑝 )
87 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
88 3 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
89 fveq2 ⊢ ( 𝐺 = 0𝑝 → ( deg ‘ 𝐺 ) = ( deg ‘ 0𝑝 ) )
90 89 83 eqtrdi ⊢ ( 𝐺 = 0𝑝 → ( deg ‘ 𝐺 ) = 0 )
91 1 90 eqtrid ⊢ ( 𝐺 = 0𝑝 → 𝑁 = 0 )
92 91 necon3i ⊢ ( 𝑁 ≠ 0 → 𝐺 ≠ 0𝑝 )
93 88 92 syl ⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝐺 ≠ 0𝑝 )
95 94 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → 𝐺 ≠ 0𝑝 )
96 eqid ⊢ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) )
97 96 1 dgrmul ⊢ ( ( ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ≠ 0𝑝 ) ∧ ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∘f · 𝐺 ) ) = ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) + 𝑁 ) )
98 74 86 87 95 97 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∘f · 𝐺 ) ) = ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) + 𝑁 ) )
99 nncn ⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℂ )
100 99 adantl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝑑 ∈ ℂ )
101 38 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝑁 ∈ ℂ )
102 100 101 adddirp1d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( 𝑑 + 1 ) · 𝑁 ) = ( ( 𝑑 · 𝑁 ) + 𝑁 ) )
103 102 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( ( 𝑑 + 1 ) · 𝑁 ) = ( ( 𝑑 · 𝑁 ) + 𝑁 ) )
104 57 98 103 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( ( 𝑑 + 1 ) · 𝑁 ) = ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ∘f · 𝐺 ) ) )
105 55 104 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) = ( ( 𝑑 + 1 ) · 𝑁 ) )
106 105 ex ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) = ( ( 𝑑 + 1 ) · 𝑁 ) ) )
107 106 expcom ⊢ ( 𝑑 ∈ ℕ → ( 𝜑 → ( ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) = ( ( 𝑑 + 1 ) · 𝑁 ) ) ) )
108 107 a2d ⊢ ( 𝑑 ∈ ℕ → ( ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑑 ) ) ) = ( 𝑑 · 𝑁 ) ) → ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ ( 𝑑 + 1 ) ) ) ) = ( ( 𝑑 + 1 ) · 𝑁 ) ) ) )
109 10 16 22 28 40 108 nnind ⊢ ( 𝑀 ∈ ℕ → ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝑀 · 𝑁 ) ) )
110 2 109 mpcom ⊢ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝑀 · 𝑁 ) )