Metamath Proof Explorer


Theorem dgrcolem2

Description: Lemma for dgrco . (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses dgrco.1 𝑀 = ( deg ‘ 𝐹 )
dgrco.2 𝑁 = ( deg ‘ 𝐺 )
dgrco.3 ( 𝜑𝐹 ∈ ( Poly ‘ 𝑆 ) )
dgrco.4 ( 𝜑𝐺 ∈ ( Poly ‘ 𝑆 ) )
dgrco.5 𝐴 = ( coeff ‘ 𝐹 )
dgrco.6 ( 𝜑𝐷 ∈ ℕ0 )
dgrco.7 ( 𝜑𝑀 = ( 𝐷 + 1 ) )
dgrco.8 ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝐷 → ( deg ‘ ( 𝑓𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
Assertion dgrcolem2 ( 𝜑 → ( deg ‘ ( 𝐹𝐺 ) ) = ( 𝑀 · 𝑁 ) )

Proof

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