Proof of Theorem plyrem
| Step | Hyp | Ref
| Expression |
| 1 | | plyssc 26239 |
. . . . . . . 8
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
| 2 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐹 ∈ (Poly‘𝑆)) |
| 3 | 1, 2 | sselid 3981 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐹 ∈
(Poly‘ℂ)) |
| 4 | | plyrem.1 |
. . . . . . . . . 10
⊢ 𝐺 = (Xp
∘f − (ℂ × {𝐴})) |
| 5 | 4 | plyremlem 26346 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝐺 ∈ (Poly‘ℂ)
∧ (deg‘𝐺) = 1
∧ (◡𝐺 “ {0}) = {𝐴})) |
| 6 | 5 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐺 ∈ (Poly‘ℂ) ∧
(deg‘𝐺) = 1 ∧
(◡𝐺 “ {0}) = {𝐴})) |
| 7 | 6 | simp1d 1143 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐺 ∈
(Poly‘ℂ)) |
| 8 | 6 | simp2d 1144 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝐺) = 1) |
| 9 | | ax-1ne0 11224 |
. . . . . . . . . 10
⊢ 1 ≠
0 |
| 10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 1 ≠
0) |
| 11 | 8, 10 | eqnetrd 3008 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝐺) ≠ 0) |
| 12 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝐺 = 0𝑝 →
(deg‘𝐺) =
(deg‘0𝑝)) |
| 13 | | dgr0 26302 |
. . . . . . . . . 10
⊢
(deg‘0𝑝) = 0 |
| 14 | 12, 13 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝐺 = 0𝑝 →
(deg‘𝐺) =
0) |
| 15 | 14 | necon3i 2973 |
. . . . . . . 8
⊢
((deg‘𝐺) ≠
0 → 𝐺 ≠
0𝑝) |
| 16 | 11, 15 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐺 ≠
0𝑝) |
| 17 | | plyrem.2 |
. . . . . . . 8
⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f ·
(𝐹 quot 𝐺))) |
| 18 | 17 | quotdgr 26345 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) |
| 19 | 3, 7, 16, 18 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) |
| 20 | | 0lt1 11785 |
. . . . . . . 8
⊢ 0 <
1 |
| 21 | 20, 8 | breqtrrid 5181 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 0 <
(deg‘𝐺)) |
| 22 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑅 = 0𝑝 →
(deg‘𝑅) =
(deg‘0𝑝)) |
| 23 | 22, 13 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑅 = 0𝑝 →
(deg‘𝑅) =
0) |
| 24 | 23 | breq1d 5153 |
. . . . . . 7
⊢ (𝑅 = 0𝑝 →
((deg‘𝑅) <
(deg‘𝐺) ↔ 0 <
(deg‘𝐺))) |
| 25 | 21, 24 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅 = 0𝑝 →
(deg‘𝑅) <
(deg‘𝐺))) |
| 26 | | pm2.62 900 |
. . . . . 6
⊢ ((𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)) →
((𝑅 = 0𝑝
→ (deg‘𝑅) <
(deg‘𝐺)) →
(deg‘𝑅) <
(deg‘𝐺))) |
| 27 | 19, 25, 26 | sylc 65 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝑅) < (deg‘𝐺)) |
| 28 | 27, 8 | breqtrd 5169 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝑅) < 1) |
| 29 | | quotcl2 26344 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) ∈
(Poly‘ℂ)) |
| 30 | 3, 7, 16, 29 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹 quot 𝐺) ∈
(Poly‘ℂ)) |
| 31 | | plymulcl 26260 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (Poly‘ℂ)
∧ (𝐹 quot 𝐺) ∈ (Poly‘ℂ))
→ (𝐺
∘f · (𝐹 quot 𝐺)) ∈
(Poly‘ℂ)) |
| 32 | 7, 30, 31 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐺 ∘f · (𝐹 quot 𝐺)) ∈
(Poly‘ℂ)) |
| 33 | | plysubcl 26261 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝐺
∘f · (𝐹 quot 𝐺)) ∈ (Poly‘ℂ)) →
(𝐹 ∘f
− (𝐺
∘f · (𝐹 quot 𝐺))) ∈
(Poly‘ℂ)) |
| 34 | 3, 32, 33 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹 ∘f − (𝐺 ∘f ·
(𝐹 quot 𝐺))) ∈
(Poly‘ℂ)) |
| 35 | 17, 34 | eqeltrid 2845 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝑅 ∈
(Poly‘ℂ)) |
| 36 | | dgrcl 26272 |
. . . . . 6
⊢ (𝑅 ∈ (Poly‘ℂ)
→ (deg‘𝑅) ∈
ℕ0) |
| 37 | 35, 36 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝑅) ∈
ℕ0) |
| 38 | | nn0lt10b 12680 |
. . . . 5
⊢
((deg‘𝑅)
∈ ℕ0 → ((deg‘𝑅) < 1 ↔ (deg‘𝑅) = 0)) |
| 39 | 37, 38 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((deg‘𝑅) < 1 ↔ (deg‘𝑅) = 0)) |
| 40 | 28, 39 | mpbid 232 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝑅) = 0) |
| 41 | | 0dgrb 26285 |
. . . 4
⊢ (𝑅 ∈ (Poly‘ℂ)
→ ((deg‘𝑅) = 0
↔ 𝑅 = (ℂ ×
{(𝑅‘0)}))) |
| 42 | 35, 41 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((deg‘𝑅) = 0 ↔ 𝑅 = (ℂ × {(𝑅‘0)}))) |
| 43 | 40, 42 | mpbid 232 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝑅 = (ℂ × {(𝑅‘0)})) |
| 44 | 43 | fveq1d 6908 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅‘𝐴) = ((ℂ × {(𝑅‘0)})‘𝐴)) |
| 45 | 17 | fveq1i 6907 |
. . . . . . 7
⊢ (𝑅‘𝐴) = ((𝐹 ∘f − (𝐺 ∘f ·
(𝐹 quot 𝐺)))‘𝐴) |
| 46 | | plyf 26237 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
| 47 | 46 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐹:ℂ⟶ℂ) |
| 48 | 47 | ffnd 6737 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐹 Fn ℂ) |
| 49 | | plyf 26237 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ (Poly‘ℂ)
→ 𝐺:ℂ⟶ℂ) |
| 50 | 7, 49 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐺:ℂ⟶ℂ) |
| 51 | 50 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐺 Fn ℂ) |
| 52 | | plyf 26237 |
. . . . . . . . . . . 12
⊢ ((𝐹 quot 𝐺) ∈ (Poly‘ℂ) → (𝐹 quot 𝐺):ℂ⟶ℂ) |
| 53 | 30, 52 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹 quot 𝐺):ℂ⟶ℂ) |
| 54 | 53 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹 quot 𝐺) Fn ℂ) |
| 55 | | cnex 11236 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
| 56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ℂ ∈
V) |
| 57 | | inidm 4227 |
. . . . . . . . . 10
⊢ (ℂ
∩ ℂ) = ℂ |
| 58 | 51, 54, 56, 56, 57 | offn 7710 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐺 ∘f · (𝐹 quot 𝐺)) Fn ℂ) |
| 59 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) ∧ 𝐴 ∈ ℂ) → (𝐹‘𝐴) = (𝐹‘𝐴)) |
| 60 | 6 | simp3d 1145 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (◡𝐺 “ {0}) = {𝐴}) |
| 61 | | ssun1 4178 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐺 “ {0}) ⊆ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})) |
| 62 | 60, 61 | eqsstrrdi 4029 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → {𝐴} ⊆ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0}))) |
| 63 | | snssg 4783 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})) ↔ {𝐴} ⊆ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})))) |
| 64 | 63 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})) ↔ {𝐴} ⊆ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})))) |
| 65 | 62, 64 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0}))) |
| 66 | | ofmulrt 26323 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
∈ V ∧ 𝐺:ℂ⟶ℂ ∧ (𝐹 quot 𝐺):ℂ⟶ℂ) → (◡(𝐺 ∘f · (𝐹 quot 𝐺)) “ {0}) = ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0}))) |
| 67 | 56, 50, 53, 66 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (◡(𝐺 ∘f · (𝐹 quot 𝐺)) “ {0}) = ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0}))) |
| 68 | 65, 67 | eleqtrrd 2844 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ (◡(𝐺 ∘f · (𝐹 quot 𝐺)) “ {0})) |
| 69 | | fniniseg 7080 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∘f ·
(𝐹 quot 𝐺)) Fn ℂ → (𝐴 ∈ (◡(𝐺 ∘f · (𝐹 quot 𝐺)) “ {0}) ↔ (𝐴 ∈ ℂ ∧ ((𝐺 ∘f · (𝐹 quot 𝐺))‘𝐴) = 0))) |
| 70 | 58, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ (◡(𝐺 ∘f · (𝐹 quot 𝐺)) “ {0}) ↔ (𝐴 ∈ ℂ ∧ ((𝐺 ∘f · (𝐹 quot 𝐺))‘𝐴) = 0))) |
| 71 | 68, 70 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ ℂ ∧ ((𝐺 ∘f · (𝐹 quot 𝐺))‘𝐴) = 0)) |
| 72 | 71 | simprd 495 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((𝐺 ∘f · (𝐹 quot 𝐺))‘𝐴) = 0) |
| 73 | 72 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) ∧ 𝐴 ∈ ℂ) → ((𝐺 ∘f · (𝐹 quot 𝐺))‘𝐴) = 0) |
| 74 | 48, 58, 56, 56, 57, 59, 73 | ofval 7708 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) ∧ 𝐴 ∈ ℂ) → ((𝐹 ∘f − (𝐺 ∘f ·
(𝐹 quot 𝐺)))‘𝐴) = ((𝐹‘𝐴) − 0)) |
| 75 | 74 | anabss3 675 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((𝐹 ∘f − (𝐺 ∘f ·
(𝐹 quot 𝐺)))‘𝐴) = ((𝐹‘𝐴) − 0)) |
| 76 | 45, 75 | eqtrid 2789 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅‘𝐴) = ((𝐹‘𝐴) − 0)) |
| 77 | 46 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹‘𝐴) ∈ ℂ) |
| 78 | 77 | subid1d 11609 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((𝐹‘𝐴) − 0) = (𝐹‘𝐴)) |
| 79 | 76, 78 | eqtrd 2777 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅‘𝐴) = (𝐹‘𝐴)) |
| 80 | | fvex 6919 |
. . . . . . 7
⊢ (𝑅‘0) ∈
V |
| 81 | 80 | fvconst2 7224 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((ℂ
× {(𝑅‘0)})‘𝐴) = (𝑅‘0)) |
| 82 | 81 | adantl 481 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((ℂ ×
{(𝑅‘0)})‘𝐴) = (𝑅‘0)) |
| 83 | 44, 79, 82 | 3eqtr3d 2785 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹‘𝐴) = (𝑅‘0)) |
| 84 | 83 | sneqd 4638 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → {(𝐹‘𝐴)} = {(𝑅‘0)}) |
| 85 | 84 | xpeq2d 5715 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (ℂ ×
{(𝐹‘𝐴)}) = (ℂ × {(𝑅‘0)})) |
| 86 | 43, 85 | eqtr4d 2780 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝑅 = (ℂ × {(𝐹‘𝐴)})) |