# 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 ${⊢}{N}=\mathrm{deg}\left({G}\right)$
dgrcolem1.2 ${⊢}{\phi }\to {M}\in ℕ$
dgrcolem1.3 ${⊢}{\phi }\to {N}\in ℕ$
dgrcolem1.4 ${⊢}{\phi }\to {G}\in \mathrm{Poly}\left({S}\right)$
Assertion dgrcolem1 ${⊢}{\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{M}}\right)\right)={M}\cdot {N}$

### Proof

Step Hyp Ref Expression
1 dgrcolem1.1 ${⊢}{N}=\mathrm{deg}\left({G}\right)$
2 dgrcolem1.2 ${⊢}{\phi }\to {M}\in ℕ$
3 dgrcolem1.3 ${⊢}{\phi }\to {N}\in ℕ$
4 dgrcolem1.4 ${⊢}{\phi }\to {G}\in \mathrm{Poly}\left({S}\right)$
5 oveq2 ${⊢}{y}=1\to {{G}\left({x}\right)}^{{y}}={{G}\left({x}\right)}^{1}$
6 5 mpteq2dv ${⊢}{y}=1\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)$
7 6 fveq2d ${⊢}{y}=1\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)\right)$
8 oveq1 ${⊢}{y}=1\to {y}\cdot {N}=1\cdot {N}$
9 7 8 eqeq12d ${⊢}{y}=1\to \left(\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)={y}\cdot {N}↔\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)\right)=1\cdot {N}\right)$
10 9 imbi2d ${⊢}{y}=1\to \left(\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)={y}\cdot {N}\right)↔\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)\right)=1\cdot {N}\right)\right)$
11 oveq2 ${⊢}{y}={d}\to {{G}\left({x}\right)}^{{y}}={{G}\left({x}\right)}^{{d}}$
12 11 mpteq2dv ${⊢}{y}={d}\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)$
13 12 fveq2d ${⊢}{y}={d}\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)$
14 oveq1 ${⊢}{y}={d}\to {y}\cdot {N}={d}\cdot {N}$
15 13 14 eqeq12d ${⊢}{y}={d}\to \left(\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)={y}\cdot {N}↔\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)$
16 15 imbi2d ${⊢}{y}={d}\to \left(\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)={y}\cdot {N}\right)↔\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\right)$
17 oveq2 ${⊢}{y}={d}+1\to {{G}\left({x}\right)}^{{y}}={{G}\left({x}\right)}^{{d}+1}$
18 17 mpteq2dv ${⊢}{y}={d}+1\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)$
19 18 fveq2d ${⊢}{y}={d}+1\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)$
20 oveq1 ${⊢}{y}={d}+1\to {y}\cdot {N}=\left({d}+1\right)\cdot {N}$
21 19 20 eqeq12d ${⊢}{y}={d}+1\to \left(\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)={y}\cdot {N}↔\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)=\left({d}+1\right)\cdot {N}\right)$
22 21 imbi2d ${⊢}{y}={d}+1\to \left(\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)={y}\cdot {N}\right)↔\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)=\left({d}+1\right)\cdot {N}\right)\right)$
23 oveq2 ${⊢}{y}={M}\to {{G}\left({x}\right)}^{{y}}={{G}\left({x}\right)}^{{M}}$
24 23 mpteq2dv ${⊢}{y}={M}\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{M}}\right)$
25 24 fveq2d ${⊢}{y}={M}\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{M}}\right)\right)$
26 oveq1 ${⊢}{y}={M}\to {y}\cdot {N}={M}\cdot {N}$
27 25 26 eqeq12d ${⊢}{y}={M}\to \left(\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)={y}\cdot {N}↔\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{M}}\right)\right)={M}\cdot {N}\right)$
28 27 imbi2d ${⊢}{y}={M}\to \left(\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{y}}\right)\right)={y}\cdot {N}\right)↔\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{M}}\right)\right)={M}\cdot {N}\right)\right)$
29 plyf ${⊢}{G}\in \mathrm{Poly}\left({S}\right)\to {G}:ℂ⟶ℂ$
30 4 29 syl ${⊢}{\phi }\to {G}:ℂ⟶ℂ$
31 30 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {G}\left({x}\right)\in ℂ$
32 31 exp1d ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to {{G}\left({x}\right)}^{1}={G}\left({x}\right)$
33 32 mpteq2dva ${⊢}{\phi }\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)=\left({x}\in ℂ⟼{G}\left({x}\right)\right)$
34 30 feqmptd ${⊢}{\phi }\to {G}=\left({x}\in ℂ⟼{G}\left({x}\right)\right)$
35 33 34 eqtr4d ${⊢}{\phi }\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)={G}$
36 35 fveq2d ${⊢}{\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)\right)=\mathrm{deg}\left({G}\right)$
37 36 1 syl6eqr ${⊢}{\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)\right)={N}$
38 3 nncnd ${⊢}{\phi }\to {N}\in ℂ$
39 38 mulid2d ${⊢}{\phi }\to 1\cdot {N}={N}$
40 37 39 eqtr4d ${⊢}{\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{1}\right)\right)=1\cdot {N}$
41 31 adantlr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge {x}\in ℂ\right)\to {G}\left({x}\right)\in ℂ$
42 nnnn0 ${⊢}{d}\in ℕ\to {d}\in {ℕ}_{0}$
43 42 adantl ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {d}\in {ℕ}_{0}$
44 43 adantr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge {x}\in ℂ\right)\to {d}\in {ℕ}_{0}$
45 41 44 expp1d ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge {x}\in ℂ\right)\to {{G}\left({x}\right)}^{{d}+1}={{G}\left({x}\right)}^{{d}}{G}\left({x}\right)$
46 45 mpteq2dva ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}{G}\left({x}\right)\right)$
47 cnex ${⊢}ℂ\in \mathrm{V}$
48 47 a1i ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to ℂ\in \mathrm{V}$
49 ovexd ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge {x}\in ℂ\right)\to {{G}\left({x}\right)}^{{d}}\in \mathrm{V}$
50 eqidd ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)$
51 34 adantr ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {G}=\left({x}\in ℂ⟼{G}\left({x}\right)\right)$
52 48 49 41 50 51 offval2 ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right){×}_{f}{G}=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}{G}\left({x}\right)\right)$
53 46 52 eqtr4d ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right){×}_{f}{G}$
54 53 fveq2d ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right){×}_{f}{G}\right)$
55 54 adantr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right){×}_{f}{G}\right)$
56 oveq1 ${⊢}\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)+{N}={d}\cdot {N}+{N}$
57 56 adantl ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)+{N}={d}\cdot {N}+{N}$
58 eqidd ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({y}\in ℂ⟼{{y}}^{{d}}\right)=\left({y}\in ℂ⟼{{y}}^{{d}}\right)$
59 oveq1 ${⊢}{y}={G}\left({x}\right)\to {{y}}^{{d}}={{G}\left({x}\right)}^{{d}}$
60 41 51 58 59 fmptco ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({y}\in ℂ⟼{{y}}^{{d}}\right)\circ {G}=\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)$
61 ssidd ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to ℂ\subseteq ℂ$
62 1cnd ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to 1\in ℂ$
63 plypow ${⊢}\left(ℂ\subseteq ℂ\wedge 1\in ℂ\wedge {d}\in {ℕ}_{0}\right)\to \left({y}\in ℂ⟼{{y}}^{{d}}\right)\in \mathrm{Poly}\left(ℂ\right)$
64 61 62 43 63 syl3anc ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({y}\in ℂ⟼{{y}}^{{d}}\right)\in \mathrm{Poly}\left(ℂ\right)$
65 plyssc ${⊢}\mathrm{Poly}\left({S}\right)\subseteq \mathrm{Poly}\left(ℂ\right)$
66 4 adantr ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {G}\in \mathrm{Poly}\left({S}\right)$
67 65 66 sseldi ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {G}\in \mathrm{Poly}\left(ℂ\right)$
68 addcl ${⊢}\left({z}\in ℂ\wedge {w}\in ℂ\right)\to {z}+{w}\in ℂ$
69 68 adantl ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \left({z}\in ℂ\wedge {w}\in ℂ\right)\right)\to {z}+{w}\in ℂ$
70 mulcl ${⊢}\left({z}\in ℂ\wedge {w}\in ℂ\right)\to {z}{w}\in ℂ$
71 70 adantl ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \left({z}\in ℂ\wedge {w}\in ℂ\right)\right)\to {z}{w}\in ℂ$
72 64 67 69 71 plyco ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({y}\in ℂ⟼{{y}}^{{d}}\right)\circ {G}\in \mathrm{Poly}\left(ℂ\right)$
73 60 72 eqeltrrd ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\in \mathrm{Poly}\left(ℂ\right)$
74 73 adantr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\in \mathrm{Poly}\left(ℂ\right)$
75 simpr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}$
76 simpr ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {d}\in ℕ$
77 3 adantr ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {N}\in ℕ$
78 76 77 nnmulcld ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {d}\cdot {N}\in ℕ$
79 78 nnne0d ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {d}\cdot {N}\ne 0$
80 79 adantr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to {d}\cdot {N}\ne 0$
81 75 80 eqnetrd ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)\ne 0$
82 fveq2 ${⊢}\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)={0}_{𝑝}\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)=\mathrm{deg}\left({0}_{𝑝}\right)$
83 dgr0 ${⊢}\mathrm{deg}\left({0}_{𝑝}\right)=0$
84 82 83 syl6eq ${⊢}\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)={0}_{𝑝}\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)=0$
85 84 necon3i ${⊢}\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)\ne 0\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\ne {0}_{𝑝}$
86 81 85 syl ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\ne {0}_{𝑝}$
87 67 adantr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to {G}\in \mathrm{Poly}\left(ℂ\right)$
88 3 nnne0d ${⊢}{\phi }\to {N}\ne 0$
89 fveq2 ${⊢}{G}={0}_{𝑝}\to \mathrm{deg}\left({G}\right)=\mathrm{deg}\left({0}_{𝑝}\right)$
90 89 83 syl6eq ${⊢}{G}={0}_{𝑝}\to \mathrm{deg}\left({G}\right)=0$
91 1 90 syl5eq ${⊢}{G}={0}_{𝑝}\to {N}=0$
92 91 necon3i ${⊢}{N}\ne 0\to {G}\ne {0}_{𝑝}$
93 88 92 syl ${⊢}{\phi }\to {G}\ne {0}_{𝑝}$
94 93 adantr ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {G}\ne {0}_{𝑝}$
95 94 adantr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to {G}\ne {0}_{𝑝}$
96 eqid ${⊢}\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)$
97 96 1 dgrmul ${⊢}\left(\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\in \mathrm{Poly}\left(ℂ\right)\wedge \left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\ne {0}_{𝑝}\right)\wedge \left({G}\in \mathrm{Poly}\left(ℂ\right)\wedge {G}\ne {0}_{𝑝}\right)\right)\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right){×}_{f}{G}\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)+{N}$
98 74 86 87 95 97 syl22anc ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right){×}_{f}{G}\right)=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)+{N}$
99 nncn ${⊢}{d}\in ℕ\to {d}\in ℂ$
100 99 adantl ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {d}\in ℂ$
101 38 adantr ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to {N}\in ℂ$
102 100 101 adddirp1d ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left({d}+1\right)\cdot {N}={d}\cdot {N}+{N}$
103 102 adantr ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \left({d}+1\right)\cdot {N}={d}\cdot {N}+{N}$
104 57 98 103 3eqtr4rd ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \left({d}+1\right)\cdot {N}=\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right){×}_{f}{G}\right)$
105 55 104 eqtr4d ${⊢}\left(\left({\phi }\wedge {d}\in ℕ\right)\wedge \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)=\left({d}+1\right)\cdot {N}$
106 105 ex ${⊢}\left({\phi }\wedge {d}\in ℕ\right)\to \left(\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)=\left({d}+1\right)\cdot {N}\right)$
107 106 expcom ${⊢}{d}\in ℕ\to \left({\phi }\to \left(\mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)=\left({d}+1\right)\cdot {N}\right)\right)$
108 107 a2d ${⊢}{d}\in ℕ\to \left(\left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}}\right)\right)={d}\cdot {N}\right)\to \left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{d}+1}\right)\right)=\left({d}+1\right)\cdot {N}\right)\right)$
109 10 16 22 28 40 108 nnind ${⊢}{M}\in ℕ\to \left({\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{M}}\right)\right)={M}\cdot {N}\right)$
110 2 109 mpcom ${⊢}{\phi }\to \mathrm{deg}\left(\left({x}\in ℂ⟼{{G}\left({x}\right)}^{{M}}\right)\right)={M}\cdot {N}$