| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | plyssc 26239 | . . 3
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) | 
| 2 |  | dgrco.3 | . . 3
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) | 
| 3 | 1, 2 | sselid 3981 | . 2
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℂ)) | 
| 4 |  | dgrco.1 | . . . 4
⊢ 𝑀 = (deg‘𝐹) | 
| 5 |  | dgrcl 26272 | . . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) | 
| 6 | 2, 5 | syl 17 | . . . 4
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) | 
| 7 | 4, 6 | eqeltrid 2845 | . . 3
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 8 |  | breq2 5147 | . . . . . . 7
⊢ (𝑥 = 0 → ((deg‘𝑓) ≤ 𝑥 ↔ (deg‘𝑓) ≤ 0)) | 
| 9 | 8 | imbi1d 341 | . . . . . 6
⊢ (𝑥 = 0 → (((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ((deg‘𝑓) ≤ 0 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 10 | 9 | ralbidv 3178 | . . . . 5
⊢ (𝑥 = 0 → (∀𝑓 ∈
(Poly‘ℂ)((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 0 →
(deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 11 | 10 | imbi2d 340 | . . . 4
⊢ (𝑥 = 0 → ((𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) ↔ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 0 →
(deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))))) | 
| 12 |  | breq2 5147 | . . . . . . 7
⊢ (𝑥 = 𝑑 → ((deg‘𝑓) ≤ 𝑥 ↔ (deg‘𝑓) ≤ 𝑑)) | 
| 13 | 12 | imbi1d 341 | . . . . . 6
⊢ (𝑥 = 𝑑 → (((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 14 | 13 | ralbidv 3178 | . . . . 5
⊢ (𝑥 = 𝑑 → (∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 15 | 14 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑑 → ((𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) ↔ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))))) | 
| 16 |  | breq2 5147 | . . . . . . 7
⊢ (𝑥 = (𝑑 + 1) → ((deg‘𝑓) ≤ 𝑥 ↔ (deg‘𝑓) ≤ (𝑑 + 1))) | 
| 17 | 16 | imbi1d 341 | . . . . . 6
⊢ (𝑥 = (𝑑 + 1) → (((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 18 | 17 | ralbidv 3178 | . . . . 5
⊢ (𝑥 = (𝑑 + 1) → (∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 19 | 18 | imbi2d 340 | . . . 4
⊢ (𝑥 = (𝑑 + 1) → ((𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) ↔ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))))) | 
| 20 |  | breq2 5147 | . . . . . . 7
⊢ (𝑥 = 𝑀 → ((deg‘𝑓) ≤ 𝑥 ↔ (deg‘𝑓) ≤ 𝑀)) | 
| 21 | 20 | imbi1d 341 | . . . . . 6
⊢ (𝑥 = 𝑀 → (((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ((deg‘𝑓) ≤ 𝑀 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 22 | 21 | ralbidv 3178 | . . . . 5
⊢ (𝑥 = 𝑀 → (∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑀 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 23 | 22 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑀 → ((𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑥 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) ↔ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑀 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))))) | 
| 24 |  | dgrco.2 | . . . . . . . . . . . 12
⊢ 𝑁 = (deg‘𝐺) | 
| 25 |  | dgrco.4 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) | 
| 26 |  | dgrcl 26272 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐺) ∈
ℕ0) | 
| 28 | 24, 27 | eqeltrid 2845 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 29 | 28 | nn0cnd 12589 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 30 | 29 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ 𝑁 ∈
ℂ) | 
| 31 | 30 | mul02d 11459 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ (0 · 𝑁) =
0) | 
| 32 |  | simprr 773 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ (deg‘𝑓) ≤
0) | 
| 33 |  | dgrcl 26272 | . . . . . . . . . . . 12
⊢ (𝑓 ∈ (Poly‘ℂ)
→ (deg‘𝑓) ∈
ℕ0) | 
| 34 | 33 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ (deg‘𝑓) ∈
ℕ0) | 
| 35 | 34 | nn0ge0d 12590 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ 0 ≤ (deg‘𝑓)) | 
| 36 | 34 | nn0red 12588 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ (deg‘𝑓) ∈
ℝ) | 
| 37 |  | 0re 11263 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ | 
| 38 |  | letri3 11346 | . . . . . . . . . . 11
⊢
(((deg‘𝑓)
∈ ℝ ∧ 0 ∈ ℝ) → ((deg‘𝑓) = 0 ↔ ((deg‘𝑓) ≤ 0 ∧ 0 ≤ (deg‘𝑓)))) | 
| 39 | 36, 37, 38 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ ((deg‘𝑓) = 0
↔ ((deg‘𝑓) ≤
0 ∧ 0 ≤ (deg‘𝑓)))) | 
| 40 | 32, 35, 39 | mpbir2and 713 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ (deg‘𝑓) =
0) | 
| 41 | 40 | oveq1d 7446 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ ((deg‘𝑓)
· 𝑁) = (0 ·
𝑁)) | 
| 42 | 31, 41, 40 | 3eqtr4d 2787 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ ((deg‘𝑓)
· 𝑁) =
(deg‘𝑓)) | 
| 43 |  | fconstmpt 5747 | . . . . . . . . 9
⊢ (ℂ
× {(𝑓‘0)}) =
(𝑦 ∈ ℂ ↦
(𝑓‘0)) | 
| 44 |  | 0dgrb 26285 | . . . . . . . . . . 11
⊢ (𝑓 ∈ (Poly‘ℂ)
→ ((deg‘𝑓) = 0
↔ 𝑓 = (ℂ ×
{(𝑓‘0)}))) | 
| 45 | 44 | ad2antrl 728 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ ((deg‘𝑓) = 0
↔ 𝑓 = (ℂ ×
{(𝑓‘0)}))) | 
| 46 | 40, 45 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ 𝑓 = (ℂ ×
{(𝑓‘0)})) | 
| 47 | 25 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ 𝐺 ∈
(Poly‘𝑆)) | 
| 48 |  | plyf 26237 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ) | 
| 49 | 47, 48 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ 𝐺:ℂ⟶ℂ) | 
| 50 | 49 | ffvelcdmda 7104 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
∧ 𝑦 ∈ ℂ)
→ (𝐺‘𝑦) ∈
ℂ) | 
| 51 | 49 | feqmptd 6977 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ 𝐺 = (𝑦 ∈ ℂ ↦ (𝐺‘𝑦))) | 
| 52 |  | fconstmpt 5747 | . . . . . . . . . . 11
⊢ (ℂ
× {(𝑓‘0)}) =
(𝑥 ∈ ℂ ↦
(𝑓‘0)) | 
| 53 | 46, 52 | eqtrdi 2793 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ 𝑓 = (𝑥 ∈ ℂ ↦ (𝑓‘0))) | 
| 54 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑦) → (𝑓‘0) = (𝑓‘0)) | 
| 55 | 50, 51, 53, 54 | fmptco 7149 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ (𝑓 ∘ 𝐺) = (𝑦 ∈ ℂ ↦ (𝑓‘0))) | 
| 56 | 43, 46, 55 | 3eqtr4a 2803 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ 𝑓 = (𝑓 ∘ 𝐺)) | 
| 57 | 56 | fveq2d 6910 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ (deg‘𝑓) =
(deg‘(𝑓 ∘ 𝐺))) | 
| 58 | 42, 57 | eqtr2d 2778 | . . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘ℂ) ∧
(deg‘𝑓) ≤ 0))
→ (deg‘(𝑓
∘ 𝐺)) =
((deg‘𝑓) ·
𝑁)) | 
| 59 | 58 | expr 456 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (Poly‘ℂ)) →
((deg‘𝑓) ≤ 0
→ (deg‘(𝑓
∘ 𝐺)) =
((deg‘𝑓) ·
𝑁))) | 
| 60 | 59 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 0 →
(deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 61 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (deg‘𝑓) = (deg‘𝑔)) | 
| 62 | 61 | breq1d 5153 | . . . . . . . . 9
⊢ (𝑓 = 𝑔 → ((deg‘𝑓) ≤ 𝑑 ↔ (deg‘𝑔) ≤ 𝑑)) | 
| 63 |  | coeq1 5868 | . . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑓 ∘ 𝐺) = (𝑔 ∘ 𝐺)) | 
| 64 | 63 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (deg‘(𝑓 ∘ 𝐺)) = (deg‘(𝑔 ∘ 𝐺))) | 
| 65 | 61 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((deg‘𝑓) · 𝑁) = ((deg‘𝑔) · 𝑁)) | 
| 66 | 64, 65 | eqeq12d 2753 | . . . . . . . . 9
⊢ (𝑓 = 𝑔 → ((deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁) ↔ (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) | 
| 67 | 62, 66 | imbi12d 344 | . . . . . . . 8
⊢ (𝑓 = 𝑔 → (((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) | 
| 68 | 67 | cbvralvw 3237 | . . . . . . 7
⊢
(∀𝑓 ∈
(Poly‘ℂ)((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ∀𝑔 ∈ (Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) | 
| 69 | 33 | ad2antrl 728 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → (deg‘𝑓) ∈
ℕ0) | 
| 70 | 69 | nn0red 12588 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → (deg‘𝑓) ∈ ℝ) | 
| 71 |  | nn0p1nn 12565 | . . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℕ0
→ (𝑑 + 1) ∈
ℕ) | 
| 72 | 71 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → (𝑑 + 1) ∈ ℕ) | 
| 73 | 72 | nnred 12281 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → (𝑑 + 1) ∈ ℝ) | 
| 74 | 70, 73 | leloed 11404 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → ((deg‘𝑓) ≤ (𝑑 + 1) ↔ ((deg‘𝑓) < (𝑑 + 1) ∨ (deg‘𝑓) = (𝑑 + 1)))) | 
| 75 |  | simplr 769 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → 𝑑 ∈ ℕ0) | 
| 76 |  | nn0leltp1 12677 | . . . . . . . . . . . . 13
⊢
(((deg‘𝑓)
∈ ℕ0 ∧ 𝑑 ∈ ℕ0) →
((deg‘𝑓) ≤ 𝑑 ↔ (deg‘𝑓) < (𝑑 + 1))) | 
| 77 | 69, 75, 76 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → ((deg‘𝑓) ≤ 𝑑 ↔ (deg‘𝑓) < (𝑑 + 1))) | 
| 78 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑓 → (deg‘𝑔) = (deg‘𝑓)) | 
| 79 | 78 | breq1d 5153 | . . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → ((deg‘𝑔) ≤ 𝑑 ↔ (deg‘𝑓) ≤ 𝑑)) | 
| 80 |  | coeq1 5868 | . . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑓 → (𝑔 ∘ 𝐺) = (𝑓 ∘ 𝐺)) | 
| 81 | 80 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑓 → (deg‘(𝑔 ∘ 𝐺)) = (deg‘(𝑓 ∘ 𝐺))) | 
| 82 | 78 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑓 → ((deg‘𝑔) · 𝑁) = ((deg‘𝑓) · 𝑁)) | 
| 83 | 81, 82 | eqeq12d 2753 | . . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → ((deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁) ↔ (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 84 | 79, 83 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → (((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)) ↔ ((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 85 | 84 | rspcva 3620 | . . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) → ((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 86 | 85 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → ((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 87 | 77, 86 | sylbird 260 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → ((deg‘𝑓) < (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 88 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(deg‘𝑓) =
(deg‘𝑓) | 
| 89 |  | simprll 779 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ ((𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) ∧ (deg‘𝑓) = (𝑑 + 1))) → 𝑓 ∈
(Poly‘ℂ)) | 
| 90 | 1, 25 | sselid 3981 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈
(Poly‘ℂ)) | 
| 91 | 90 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ ((𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) ∧ (deg‘𝑓) = (𝑑 + 1))) → 𝐺 ∈
(Poly‘ℂ)) | 
| 92 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(coeff‘𝑓) =
(coeff‘𝑓) | 
| 93 |  | simplr 769 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ ((𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) ∧ (deg‘𝑓) = (𝑑 + 1))) → 𝑑 ∈ ℕ0) | 
| 94 |  | simprr 773 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ ((𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) ∧ (deg‘𝑓) = (𝑑 + 1))) → (deg‘𝑓) = (𝑑 + 1)) | 
| 95 |  | simprlr 780 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ ((𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) ∧ (deg‘𝑓) = (𝑑 + 1))) → ∀𝑔 ∈ (Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) | 
| 96 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → (deg‘𝑔) = (deg‘ℎ)) | 
| 97 | 96 | breq1d 5153 | . . . . . . . . . . . . . . . 16
⊢ (𝑔 = ℎ → ((deg‘𝑔) ≤ 𝑑 ↔ (deg‘ℎ) ≤ 𝑑)) | 
| 98 |  | coeq1 5868 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = ℎ → (𝑔 ∘ 𝐺) = (ℎ ∘ 𝐺)) | 
| 99 | 98 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → (deg‘(𝑔 ∘ 𝐺)) = (deg‘(ℎ ∘ 𝐺))) | 
| 100 | 96 | oveq1d 7446 | . . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → ((deg‘𝑔) · 𝑁) = ((deg‘ℎ) · 𝑁)) | 
| 101 | 99, 100 | eqeq12d 2753 | . . . . . . . . . . . . . . . 16
⊢ (𝑔 = ℎ → ((deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁) ↔ (deg‘(ℎ ∘ 𝐺)) = ((deg‘ℎ) · 𝑁))) | 
| 102 | 97, 101 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ (𝑔 = ℎ → (((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)) ↔ ((deg‘ℎ) ≤ 𝑑 → (deg‘(ℎ ∘ 𝐺)) = ((deg‘ℎ) · 𝑁)))) | 
| 103 | 102 | cbvralvw 3237 | . . . . . . . . . . . . . 14
⊢
(∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)) ↔ ∀ℎ ∈ (Poly‘ℂ)((deg‘ℎ) ≤ 𝑑 → (deg‘(ℎ ∘ 𝐺)) = ((deg‘ℎ) · 𝑁))) | 
| 104 | 95, 103 | sylib 218 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ ((𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) ∧ (deg‘𝑓) = (𝑑 + 1))) → ∀ℎ ∈ (Poly‘ℂ)((deg‘ℎ) ≤ 𝑑 → (deg‘(ℎ ∘ 𝐺)) = ((deg‘ℎ) · 𝑁))) | 
| 105 | 88, 24, 89, 91, 92, 93, 94, 104 | dgrcolem2 26314 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ ((𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁))) ∧ (deg‘𝑓) = (𝑑 + 1))) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) | 
| 106 | 105 | expr 456 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → ((deg‘𝑓) = (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 107 | 87, 106 | jaod 860 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → (((deg‘𝑓) < (𝑑 + 1) ∨ (deg‘𝑓) = (𝑑 + 1)) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 108 | 74, 107 | sylbid 240 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑓 ∈ (Poly‘ℂ)
∧ ∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)))) → ((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 109 | 108 | expr 456 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘ℂ))
→ (∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)) → ((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 110 | 109 | ralrimdva 3154 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
(∀𝑔 ∈
(Poly‘ℂ)((deg‘𝑔) ≤ 𝑑 → (deg‘(𝑔 ∘ 𝐺)) = ((deg‘𝑔) · 𝑁)) → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 111 | 68, 110 | biimtrid 242 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
(∀𝑓 ∈
(Poly‘ℂ)((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 112 | 111 | expcom 413 | . . . . 5
⊢ (𝑑 ∈ ℕ0
→ (𝜑 →
(∀𝑓 ∈
(Poly‘ℂ)((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))))) | 
| 113 | 112 | a2d 29 | . . . 4
⊢ (𝑑 ∈ ℕ0
→ ((𝜑 →
∀𝑓 ∈
(Poly‘ℂ)((deg‘𝑓) ≤ 𝑑 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) → (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ (𝑑 + 1) → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))))) | 
| 114 | 11, 15, 19, 23, 60, 113 | nn0ind 12713 | . . 3
⊢ (𝑀 ∈ ℕ0
→ (𝜑 →
∀𝑓 ∈
(Poly‘ℂ)((deg‘𝑓) ≤ 𝑀 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))) | 
| 115 | 7, 114 | mpcom 38 | . 2
⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝑀 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) | 
| 116 | 7 | nn0red 12588 | . . 3
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 117 | 116 | leidd 11829 | . 2
⊢ (𝜑 → 𝑀 ≤ 𝑀) | 
| 118 |  | fveq2 6906 | . . . . . 6
⊢ (𝑓 = 𝐹 → (deg‘𝑓) = (deg‘𝐹)) | 
| 119 | 118, 4 | eqtr4di 2795 | . . . . 5
⊢ (𝑓 = 𝐹 → (deg‘𝑓) = 𝑀) | 
| 120 | 119 | breq1d 5153 | . . . 4
⊢ (𝑓 = 𝐹 → ((deg‘𝑓) ≤ 𝑀 ↔ 𝑀 ≤ 𝑀)) | 
| 121 |  | coeq1 5868 | . . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓 ∘ 𝐺) = (𝐹 ∘ 𝐺)) | 
| 122 | 121 | fveq2d 6910 | . . . . 5
⊢ (𝑓 = 𝐹 → (deg‘(𝑓 ∘ 𝐺)) = (deg‘(𝐹 ∘ 𝐺))) | 
| 123 | 119 | oveq1d 7446 | . . . . 5
⊢ (𝑓 = 𝐹 → ((deg‘𝑓) · 𝑁) = (𝑀 · 𝑁)) | 
| 124 | 122, 123 | eqeq12d 2753 | . . . 4
⊢ (𝑓 = 𝐹 → ((deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁) ↔ (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁))) | 
| 125 | 120, 124 | imbi12d 344 | . . 3
⊢ (𝑓 = 𝐹 → (((deg‘𝑓) ≤ 𝑀 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ (𝑀 ≤ 𝑀 → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁)))) | 
| 126 | 125 | rspcv 3618 | . 2
⊢ (𝐹 ∈ (Poly‘ℂ)
→ (∀𝑓 ∈
(Poly‘ℂ)((deg‘𝑓) ≤ 𝑀 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) → (𝑀 ≤ 𝑀 → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁)))) | 
| 127 | 3, 115, 117, 126 | syl3c 66 | 1
⊢ (𝜑 → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁)) |