| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | plyrem.1 | . . 3
⊢ 𝐺 = (Xp
∘f − (ℂ × {𝐴})) | 
| 2 |  | ssid 4006 | . . . . 5
⊢ ℂ
⊆ ℂ | 
| 3 |  | ax-1cn 11213 | . . . . 5
⊢ 1 ∈
ℂ | 
| 4 |  | plyid 26248 | . . . . 5
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈
(Poly‘ℂ)) | 
| 5 | 2, 3, 4 | mp2an 692 | . . . 4
⊢
Xp ∈ (Poly‘ℂ) | 
| 6 |  | plyconst 26245 | . . . . 5
⊢ ((ℂ
⊆ ℂ ∧ 𝐴
∈ ℂ) → (ℂ × {𝐴}) ∈
(Poly‘ℂ)) | 
| 7 | 2, 6 | mpan 690 | . . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}) ∈
(Poly‘ℂ)) | 
| 8 |  | plysubcl 26261 | . . . 4
⊢
((Xp ∈ (Poly‘ℂ) ∧ (ℂ
× {𝐴}) ∈
(Poly‘ℂ)) → (Xp ∘f −
(ℂ × {𝐴}))
∈ (Poly‘ℂ)) | 
| 9 | 5, 7, 8 | sylancr 587 | . . 3
⊢ (𝐴 ∈ ℂ →
(Xp ∘f − (ℂ × {𝐴})) ∈
(Poly‘ℂ)) | 
| 10 | 1, 9 | eqeltrid 2845 | . 2
⊢ (𝐴 ∈ ℂ → 𝐺 ∈
(Poly‘ℂ)) | 
| 11 |  | negcl 11508 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) | 
| 12 |  | addcom 11447 | . . . . . . . . 9
⊢ ((-𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (-𝐴 + 𝑧) = (𝑧 + -𝐴)) | 
| 13 | 11, 12 | sylan 580 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (-𝐴 + 𝑧) = (𝑧 + -𝐴)) | 
| 14 |  | negsub 11557 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑧 + -𝐴) = (𝑧 − 𝐴)) | 
| 15 | 14 | ancoms 458 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 + -𝐴) = (𝑧 − 𝐴)) | 
| 16 | 13, 15 | eqtrd 2777 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (-𝐴 + 𝑧) = (𝑧 − 𝐴)) | 
| 17 | 16 | mpteq2dva 5242 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑧 ∈ ℂ ↦ (-𝐴 + 𝑧)) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝐴))) | 
| 18 |  | cnex 11236 | . . . . . . . 8
⊢ ℂ
∈ V | 
| 19 | 18 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → ℂ
∈ V) | 
| 20 |  | negex 11506 | . . . . . . . 8
⊢ -𝐴 ∈ V | 
| 21 | 20 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → -𝐴 ∈ V) | 
| 22 |  | simpr 484 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) | 
| 23 |  | fconstmpt 5747 | . . . . . . . 8
⊢ (ℂ
× {-𝐴}) = (𝑧 ∈ ℂ ↦ -𝐴) | 
| 24 | 23 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
× {-𝐴}) = (𝑧 ∈ ℂ ↦ -𝐴)) | 
| 25 |  | df-idp 26228 | . . . . . . . . 9
⊢
Xp = ( I ↾ ℂ) | 
| 26 |  | mptresid 6069 | . . . . . . . . 9
⊢ ( I
↾ ℂ) = (𝑧
∈ ℂ ↦ 𝑧) | 
| 27 | 25, 26 | eqtri 2765 | . . . . . . . 8
⊢
Xp = (𝑧 ∈ ℂ ↦ 𝑧) | 
| 28 | 27 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
Xp = (𝑧
∈ ℂ ↦ 𝑧)) | 
| 29 | 19, 21, 22, 24, 28 | offval2 7717 | . . . . . 6
⊢ (𝐴 ∈ ℂ → ((ℂ
× {-𝐴})
∘f + Xp) = (𝑧 ∈ ℂ ↦ (-𝐴 + 𝑧))) | 
| 30 |  | simpl 482 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝐴 ∈
ℂ) | 
| 31 |  | fconstmpt 5747 | . . . . . . . 8
⊢ (ℂ
× {𝐴}) = (𝑧 ∈ ℂ ↦ 𝐴) | 
| 32 | 31 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}) = (𝑧 ∈ ℂ ↦ 𝐴)) | 
| 33 | 19, 22, 30, 28, 32 | offval2 7717 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(Xp ∘f − (ℂ × {𝐴})) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝐴))) | 
| 34 | 17, 29, 33 | 3eqtr4d 2787 | . . . . 5
⊢ (𝐴 ∈ ℂ → ((ℂ
× {-𝐴})
∘f + Xp) = (Xp
∘f − (ℂ × {𝐴}))) | 
| 35 | 34, 1 | eqtr4di 2795 | . . . 4
⊢ (𝐴 ∈ ℂ → ((ℂ
× {-𝐴})
∘f + Xp) = 𝐺) | 
| 36 | 35 | fveq2d 6910 | . . 3
⊢ (𝐴 ∈ ℂ →
(deg‘((ℂ × {-𝐴}) ∘f +
Xp)) = (deg‘𝐺)) | 
| 37 |  | plyconst 26245 | . . . . 5
⊢ ((ℂ
⊆ ℂ ∧ -𝐴
∈ ℂ) → (ℂ × {-𝐴}) ∈
(Poly‘ℂ)) | 
| 38 | 2, 11, 37 | sylancr 587 | . . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
× {-𝐴}) ∈
(Poly‘ℂ)) | 
| 39 | 5 | a1i 11 | . . . 4
⊢ (𝐴 ∈ ℂ →
Xp ∈ (Poly‘ℂ)) | 
| 40 |  | 0dgr 26284 | . . . . . 6
⊢ (-𝐴 ∈ ℂ →
(deg‘(ℂ × {-𝐴})) = 0) | 
| 41 | 11, 40 | syl 17 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(deg‘(ℂ × {-𝐴})) = 0) | 
| 42 |  | 0lt1 11785 | . . . . 5
⊢ 0 <
1 | 
| 43 | 41, 42 | eqbrtrdi 5182 | . . . 4
⊢ (𝐴 ∈ ℂ →
(deg‘(ℂ × {-𝐴})) < 1) | 
| 44 |  | eqid 2737 | . . . . 5
⊢
(deg‘(ℂ × {-𝐴})) = (deg‘(ℂ × {-𝐴})) | 
| 45 |  | dgrid 26304 | . . . . . 6
⊢
(deg‘Xp) = 1 | 
| 46 | 45 | eqcomi 2746 | . . . . 5
⊢ 1 =
(deg‘Xp) | 
| 47 | 44, 46 | dgradd2 26308 | . . . 4
⊢
(((ℂ × {-𝐴}) ∈ (Poly‘ℂ) ∧
Xp ∈ (Poly‘ℂ) ∧ (deg‘(ℂ
× {-𝐴})) < 1)
→ (deg‘((ℂ × {-𝐴}) ∘f +
Xp)) = 1) | 
| 48 | 38, 39, 43, 47 | syl3anc 1373 | . . 3
⊢ (𝐴 ∈ ℂ →
(deg‘((ℂ × {-𝐴}) ∘f +
Xp)) = 1) | 
| 49 | 36, 48 | eqtr3d 2779 | . 2
⊢ (𝐴 ∈ ℂ →
(deg‘𝐺) =
1) | 
| 50 | 1, 33 | eqtrid 2789 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → 𝐺 = (𝑧 ∈ ℂ ↦ (𝑧 − 𝐴))) | 
| 51 | 50 | fveq1d 6908 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝐺‘𝑧) = ((𝑧 ∈ ℂ ↦ (𝑧 − 𝐴))‘𝑧)) | 
| 52 | 51 | adantr 480 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝐺‘𝑧) = ((𝑧 ∈ ℂ ↦ (𝑧 − 𝐴))‘𝑧)) | 
| 53 |  | ovex 7464 | . . . . . . . . . 10
⊢ (𝑧 − 𝐴) ∈ V | 
| 54 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ ↦ (𝑧 − 𝐴)) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝐴)) | 
| 55 | 54 | fvmpt2 7027 | . . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧ (𝑧 − 𝐴) ∈ V) → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝐴))‘𝑧) = (𝑧 − 𝐴)) | 
| 56 | 22, 53, 55 | sylancl 586 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝐴))‘𝑧) = (𝑧 − 𝐴)) | 
| 57 | 52, 56 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝐺‘𝑧) = (𝑧 − 𝐴)) | 
| 58 | 57 | eqeq1d 2739 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐺‘𝑧) = 0 ↔ (𝑧 − 𝐴) = 0)) | 
| 59 |  | subeq0 11535 | . . . . . . . 8
⊢ ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑧 − 𝐴) = 0 ↔ 𝑧 = 𝐴)) | 
| 60 | 59 | ancoms 458 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑧 − 𝐴) = 0 ↔ 𝑧 = 𝐴)) | 
| 61 | 58, 60 | bitrd 279 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐺‘𝑧) = 0 ↔ 𝑧 = 𝐴)) | 
| 62 | 61 | pm5.32da 579 | . . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑧 ∈ ℂ ∧ (𝐺‘𝑧) = 0) ↔ (𝑧 ∈ ℂ ∧ 𝑧 = 𝐴))) | 
| 63 |  | plyf 26237 | . . . . . 6
⊢ (𝐺 ∈ (Poly‘ℂ)
→ 𝐺:ℂ⟶ℂ) | 
| 64 |  | ffn 6736 | . . . . . 6
⊢ (𝐺:ℂ⟶ℂ →
𝐺 Fn
ℂ) | 
| 65 |  | fniniseg 7080 | . . . . . 6
⊢ (𝐺 Fn ℂ → (𝑧 ∈ (◡𝐺 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐺‘𝑧) = 0))) | 
| 66 | 10, 63, 64, 65 | 4syl 19 | . . . . 5
⊢ (𝐴 ∈ ℂ → (𝑧 ∈ (◡𝐺 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐺‘𝑧) = 0))) | 
| 67 |  | eleq1a 2836 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑧 = 𝐴 → 𝑧 ∈ ℂ)) | 
| 68 | 67 | pm4.71rd 562 | . . . . 5
⊢ (𝐴 ∈ ℂ → (𝑧 = 𝐴 ↔ (𝑧 ∈ ℂ ∧ 𝑧 = 𝐴))) | 
| 69 | 62, 66, 68 | 3bitr4d 311 | . . . 4
⊢ (𝐴 ∈ ℂ → (𝑧 ∈ (◡𝐺 “ {0}) ↔ 𝑧 = 𝐴)) | 
| 70 |  | velsn 4642 | . . . 4
⊢ (𝑧 ∈ {𝐴} ↔ 𝑧 = 𝐴) | 
| 71 | 69, 70 | bitr4di 289 | . . 3
⊢ (𝐴 ∈ ℂ → (𝑧 ∈ (◡𝐺 “ {0}) ↔ 𝑧 ∈ {𝐴})) | 
| 72 | 71 | eqrdv 2735 | . 2
⊢ (𝐴 ∈ ℂ → (◡𝐺 “ {0}) = {𝐴}) | 
| 73 | 10, 49, 72 | 3jca 1129 | 1
⊢ (𝐴 ∈ ℂ → (𝐺 ∈ (Poly‘ℂ)
∧ (deg‘𝐺) = 1
∧ (◡𝐺 “ {0}) = {𝐴})) |