Proof of Theorem plyrem
Step | Hyp | Ref
| Expression |
1 | | plyssc 23760 |
. . . . . . . 8
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
2 | | simpl 472 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐹 ∈ (Poly‘𝑆)) |
3 | 1, 2 | sseldi 3566 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐹 ∈
(Poly‘ℂ)) |
4 | | plyrem.1 |
. . . . . . . . . 10
⊢ 𝐺 = (Xp
∘𝑓 − (ℂ × {𝐴})) |
5 | 4 | plyremlem 23863 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝐺 ∈ (Poly‘ℂ)
∧ (deg‘𝐺) = 1
∧ (◡𝐺 “ {0}) = {𝐴})) |
6 | 5 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐺 ∈ (Poly‘ℂ) ∧
(deg‘𝐺) = 1 ∧
(◡𝐺 “ {0}) = {𝐴})) |
7 | 6 | simp1d 1066 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐺 ∈
(Poly‘ℂ)) |
8 | 6 | simp2d 1067 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝐺) = 1) |
9 | | ax-1ne0 9884 |
. . . . . . . . . 10
⊢ 1 ≠
0 |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 1 ≠
0) |
11 | 8, 10 | eqnetrd 2849 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝐺) ≠ 0) |
12 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝐺 = 0𝑝 →
(deg‘𝐺) =
(deg‘0𝑝)) |
13 | | dgr0 23822 |
. . . . . . . . . 10
⊢
(deg‘0𝑝) = 0 |
14 | 12, 13 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝐺 = 0𝑝 →
(deg‘𝐺) =
0) |
15 | 14 | necon3i 2814 |
. . . . . . . 8
⊢
((deg‘𝐺) ≠
0 → 𝐺 ≠
0𝑝) |
16 | 11, 15 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐺 ≠
0𝑝) |
17 | | plyrem.2 |
. . . . . . . 8
⊢ 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐹 quot 𝐺))) |
18 | 17 | quotdgr 23862 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) |
19 | 3, 7, 16, 18 | syl3anc 1318 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) |
20 | | 0lt1 10429 |
. . . . . . . 8
⊢ 0 <
1 |
21 | 20, 8 | syl5breqr 4621 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 0 <
(deg‘𝐺)) |
22 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑅 = 0𝑝 →
(deg‘𝑅) =
(deg‘0𝑝)) |
23 | 22, 13 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑅 = 0𝑝 →
(deg‘𝑅) =
0) |
24 | 23 | breq1d 4593 |
. . . . . . 7
⊢ (𝑅 = 0𝑝 →
((deg‘𝑅) <
(deg‘𝐺) ↔ 0 <
(deg‘𝐺))) |
25 | 21, 24 | syl5ibrcom 236 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅 = 0𝑝 →
(deg‘𝑅) <
(deg‘𝐺))) |
26 | | pm2.62 424 |
. . . . . 6
⊢ ((𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)) →
((𝑅 = 0𝑝
→ (deg‘𝑅) <
(deg‘𝐺)) →
(deg‘𝑅) <
(deg‘𝐺))) |
27 | 19, 25, 26 | sylc 63 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝑅) < (deg‘𝐺)) |
28 | 27, 8 | breqtrd 4609 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝑅) < 1) |
29 | | quotcl2 23861 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) ∈
(Poly‘ℂ)) |
30 | 3, 7, 16, 29 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹 quot 𝐺) ∈
(Poly‘ℂ)) |
31 | | plymulcl 23781 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (Poly‘ℂ)
∧ (𝐹 quot 𝐺) ∈ (Poly‘ℂ))
→ (𝐺
∘𝑓 · (𝐹 quot 𝐺)) ∈
(Poly‘ℂ)) |
32 | 7, 30, 31 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐺 ∘𝑓 · (𝐹 quot 𝐺)) ∈
(Poly‘ℂ)) |
33 | | plysubcl 23782 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝐺
∘𝑓 · (𝐹 quot 𝐺)) ∈ (Poly‘ℂ)) →
(𝐹
∘𝑓 − (𝐺 ∘𝑓 · (𝐹 quot 𝐺))) ∈
(Poly‘ℂ)) |
34 | 3, 32, 33 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐹 quot 𝐺))) ∈
(Poly‘ℂ)) |
35 | 17, 34 | syl5eqel 2692 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝑅 ∈
(Poly‘ℂ)) |
36 | | dgrcl 23793 |
. . . . . 6
⊢ (𝑅 ∈ (Poly‘ℂ)
→ (deg‘𝑅) ∈
ℕ0) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝑅) ∈
ℕ0) |
38 | | nn0lt10b 11316 |
. . . . 5
⊢
((deg‘𝑅)
∈ ℕ0 → ((deg‘𝑅) < 1 ↔ (deg‘𝑅) = 0)) |
39 | 37, 38 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((deg‘𝑅) < 1 ↔ (deg‘𝑅) = 0)) |
40 | 28, 39 | mpbid 221 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (deg‘𝑅) = 0) |
41 | | 0dgrb 23806 |
. . . 4
⊢ (𝑅 ∈ (Poly‘ℂ)
→ ((deg‘𝑅) = 0
↔ 𝑅 = (ℂ ×
{(𝑅‘0)}))) |
42 | 35, 41 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((deg‘𝑅) = 0 ↔ 𝑅 = (ℂ × {(𝑅‘0)}))) |
43 | 40, 42 | mpbid 221 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝑅 = (ℂ × {(𝑅‘0)})) |
44 | 43 | fveq1d 6105 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅‘𝐴) = ((ℂ × {(𝑅‘0)})‘𝐴)) |
45 | 17 | fveq1i 6104 |
. . . . . . 7
⊢ (𝑅‘𝐴) = ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐹 quot 𝐺)))‘𝐴) |
46 | | plyf 23758 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
47 | 46 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐹:ℂ⟶ℂ) |
48 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
49 | 47, 48 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐹 Fn ℂ) |
50 | | plyf 23758 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ (Poly‘ℂ)
→ 𝐺:ℂ⟶ℂ) |
51 | 7, 50 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐺:ℂ⟶ℂ) |
52 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐺:ℂ⟶ℂ →
𝐺 Fn
ℂ) |
53 | 51, 52 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐺 Fn ℂ) |
54 | | plyf 23758 |
. . . . . . . . . . . 12
⊢ ((𝐹 quot 𝐺) ∈ (Poly‘ℂ) → (𝐹 quot 𝐺):ℂ⟶ℂ) |
55 | 30, 54 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹 quot 𝐺):ℂ⟶ℂ) |
56 | | ffn 5958 |
. . . . . . . . . . 11
⊢ ((𝐹 quot 𝐺):ℂ⟶ℂ → (𝐹 quot 𝐺) Fn ℂ) |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹 quot 𝐺) Fn ℂ) |
58 | | cnex 9896 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
59 | 58 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ℂ ∈
V) |
60 | | inidm 3784 |
. . . . . . . . . 10
⊢ (ℂ
∩ ℂ) = ℂ |
61 | 53, 57, 59, 59, 60 | offn 6806 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐺 ∘𝑓 · (𝐹 quot 𝐺)) Fn ℂ) |
62 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) ∧ 𝐴 ∈ ℂ) → (𝐹‘𝐴) = (𝐹‘𝐴)) |
63 | 6 | simp3d 1068 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (◡𝐺 “ {0}) = {𝐴}) |
64 | | ssun1 3738 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐺 “ {0}) ⊆ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})) |
65 | 63, 64 | syl6eqssr 3619 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → {𝐴} ⊆ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0}))) |
66 | | snssg 4268 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})) ↔ {𝐴} ⊆ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})))) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})) ↔ {𝐴} ⊆ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0})))) |
68 | 65, 67 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0}))) |
69 | | ofmulrt 23841 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
∈ V ∧ 𝐺:ℂ⟶ℂ ∧ (𝐹 quot 𝐺):ℂ⟶ℂ) → (◡(𝐺 ∘𝑓 · (𝐹 quot 𝐺)) “ {0}) = ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0}))) |
70 | 59, 51, 55, 69 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (◡(𝐺 ∘𝑓 · (𝐹 quot 𝐺)) “ {0}) = ((◡𝐺 “ {0}) ∪ (◡(𝐹 quot 𝐺) “ {0}))) |
71 | 68, 70 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ (◡(𝐺 ∘𝑓 · (𝐹 quot 𝐺)) “ {0})) |
72 | | fniniseg 6246 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∘𝑓
· (𝐹 quot 𝐺)) Fn ℂ → (𝐴 ∈ (◡(𝐺 ∘𝑓 · (𝐹 quot 𝐺)) “ {0}) ↔ (𝐴 ∈ ℂ ∧ ((𝐺 ∘𝑓 · (𝐹 quot 𝐺))‘𝐴) = 0))) |
73 | 61, 72 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ (◡(𝐺 ∘𝑓 · (𝐹 quot 𝐺)) “ {0}) ↔ (𝐴 ∈ ℂ ∧ ((𝐺 ∘𝑓 · (𝐹 quot 𝐺))‘𝐴) = 0))) |
74 | 71, 73 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐴 ∈ ℂ ∧ ((𝐺 ∘𝑓 · (𝐹 quot 𝐺))‘𝐴) = 0)) |
75 | 74 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((𝐺 ∘𝑓 · (𝐹 quot 𝐺))‘𝐴) = 0) |
76 | 75 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) ∧ 𝐴 ∈ ℂ) → ((𝐺 ∘𝑓 · (𝐹 quot 𝐺))‘𝐴) = 0) |
77 | 49, 61, 59, 59, 60, 62, 76 | ofval 6804 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) ∧ 𝐴 ∈ ℂ) → ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐹 quot 𝐺)))‘𝐴) = ((𝐹‘𝐴) − 0)) |
78 | 77 | anabss3 860 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐹 quot 𝐺)))‘𝐴) = ((𝐹‘𝐴) − 0)) |
79 | 45, 78 | syl5eq 2656 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅‘𝐴) = ((𝐹‘𝐴) − 0)) |
80 | 46 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹‘𝐴) ∈ ℂ) |
81 | 80 | subid1d 10260 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((𝐹‘𝐴) − 0) = (𝐹‘𝐴)) |
82 | 79, 81 | eqtrd 2644 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝑅‘𝐴) = (𝐹‘𝐴)) |
83 | | fvex 6113 |
. . . . . . 7
⊢ (𝑅‘0) ∈
V |
84 | 83 | fvconst2 6374 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((ℂ
× {(𝑅‘0)})‘𝐴) = (𝑅‘0)) |
85 | 84 | adantl 481 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → ((ℂ ×
{(𝑅‘0)})‘𝐴) = (𝑅‘0)) |
86 | 44, 82, 85 | 3eqtr3d 2652 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (𝐹‘𝐴) = (𝑅‘0)) |
87 | 86 | sneqd 4137 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → {(𝐹‘𝐴)} = {(𝑅‘0)}) |
88 | 87 | xpeq2d 5063 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → (ℂ ×
{(𝐹‘𝐴)}) = (ℂ × {(𝑅‘0)})) |
89 | 43, 88 | eqtr4d 2647 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝑅 = (ℂ × {(𝐹‘𝐴)})) |