Step | Hyp | Ref
| Expression |
1 | | idd 24 |
. . . 4
⊢ (𝜑 → ((𝑝 ∘f − 𝑞) = 0𝑝 →
(𝑝 ∘f
− 𝑞) =
0𝑝)) |
2 | | plydiveu.q |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑞 ∈ (Poly‘𝑆)) |
3 | | plydiv.pl |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
4 | | plydiv.tm |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
5 | | plydiv.rc |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆) |
6 | | plydiv.m1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -1 ∈ 𝑆) |
7 | | plydiv.f |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
8 | | plydiv.g |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |
9 | | plydiv.z |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ≠
0𝑝) |
10 | | plydiv.r |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f ·
𝑞)) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | plydivlem2 25042 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑞 ∈ (Poly‘𝑆)) → 𝑅 ∈ (Poly‘𝑆)) |
12 | 2, 11 | mpdan 687 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ (Poly‘𝑆)) |
13 | | plydiveu.p |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑝 ∈ (Poly‘𝑆)) |
14 | | plydiveu.t |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇 = (𝐹 ∘f − (𝐺 ∘f ·
𝑝)) |
15 | 3, 4, 5, 6, 7, 8, 9, 14 | plydivlem2 25042 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝑇 ∈ (Poly‘𝑆)) |
16 | 13, 15 | mpdan 687 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ∈ (Poly‘𝑆)) |
17 | 12, 16, 3, 4, 6 | plysub 24968 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 ∘f − 𝑇) ∈ (Poly‘𝑆)) |
18 | | dgrcl 24982 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∘f −
𝑇) ∈ (Poly‘𝑆) → (deg‘(𝑅 ∘f −
𝑇)) ∈
ℕ0) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘(𝑅 ∘f −
𝑇)) ∈
ℕ0) |
20 | 19 | nn0red 12037 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘(𝑅 ∘f −
𝑇)) ∈
ℝ) |
21 | | dgrcl 24982 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (Poly‘𝑆) → (deg‘𝑇) ∈
ℕ0) |
22 | 16, 21 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (deg‘𝑇) ∈
ℕ0) |
23 | 22 | nn0red 12037 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝑇) ∈
ℝ) |
24 | | dgrcl 24982 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ (Poly‘𝑆) → (deg‘𝑅) ∈
ℕ0) |
25 | 12, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (deg‘𝑅) ∈
ℕ0) |
26 | 25 | nn0red 12037 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝑅) ∈
ℝ) |
27 | 23, 26 | ifcld 4460 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((deg‘𝑅) ≤ (deg‘𝑇), (deg‘𝑇), (deg‘𝑅)) ∈ ℝ) |
28 | | dgrcl 24982 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
29 | 8, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝐺) ∈
ℕ0) |
30 | 29 | nn0red 12037 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐺) ∈
ℝ) |
31 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(deg‘𝑅) =
(deg‘𝑅) |
32 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(deg‘𝑇) =
(deg‘𝑇) |
33 | 31, 32 | dgrsub 25021 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ (Poly‘𝑆) ∧ 𝑇 ∈ (Poly‘𝑆)) → (deg‘(𝑅 ∘f − 𝑇)) ≤ if((deg‘𝑅) ≤ (deg‘𝑇), (deg‘𝑇), (deg‘𝑅))) |
34 | 12, 16, 33 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘(𝑅 ∘f −
𝑇)) ≤
if((deg‘𝑅) ≤
(deg‘𝑇),
(deg‘𝑇),
(deg‘𝑅))) |
35 | | plydiveu.pd |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 = 0𝑝 ∨
(deg‘𝑇) <
(deg‘𝐺))) |
36 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(coeff‘𝑇) =
(coeff‘𝑇) |
37 | 32, 36 | dgrlt 25015 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ (Poly‘𝑆) ∧ (deg‘𝐺) ∈ ℕ0)
→ ((𝑇 =
0𝑝 ∨ (deg‘𝑇) < (deg‘𝐺)) ↔ ((deg‘𝑇) ≤ (deg‘𝐺) ∧ ((coeff‘𝑇)‘(deg‘𝐺)) = 0))) |
38 | 16, 29, 37 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑇 = 0𝑝 ∨
(deg‘𝑇) <
(deg‘𝐺)) ↔
((deg‘𝑇) ≤
(deg‘𝐺) ∧
((coeff‘𝑇)‘(deg‘𝐺)) = 0))) |
39 | 35, 38 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((deg‘𝑇) ≤ (deg‘𝐺) ∧ ((coeff‘𝑇)‘(deg‘𝐺)) = 0)) |
40 | 39 | simpld 498 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝑇) ≤ (deg‘𝐺)) |
41 | | plydiveu.qd |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) |
42 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(coeff‘𝑅) =
(coeff‘𝑅) |
43 | 31, 42 | dgrlt 25015 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ (Poly‘𝑆) ∧ (deg‘𝐺) ∈ ℕ0)
→ ((𝑅 =
0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)) ↔ ((deg‘𝑅) ≤ (deg‘𝐺) ∧ ((coeff‘𝑅)‘(deg‘𝐺)) = 0))) |
44 | 12, 29, 43 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)) ↔
((deg‘𝑅) ≤
(deg‘𝐺) ∧
((coeff‘𝑅)‘(deg‘𝐺)) = 0))) |
45 | 41, 44 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((deg‘𝑅) ≤ (deg‘𝐺) ∧ ((coeff‘𝑅)‘(deg‘𝐺)) = 0)) |
46 | 45 | simpld 498 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝑅) ≤ (deg‘𝐺)) |
47 | | breq1 5033 |
. . . . . . . . . . . . . 14
⊢
((deg‘𝑇) =
if((deg‘𝑅) ≤
(deg‘𝑇),
(deg‘𝑇),
(deg‘𝑅)) →
((deg‘𝑇) ≤
(deg‘𝐺) ↔
if((deg‘𝑅) ≤
(deg‘𝑇),
(deg‘𝑇),
(deg‘𝑅)) ≤
(deg‘𝐺))) |
48 | | breq1 5033 |
. . . . . . . . . . . . . 14
⊢
((deg‘𝑅) =
if((deg‘𝑅) ≤
(deg‘𝑇),
(deg‘𝑇),
(deg‘𝑅)) →
((deg‘𝑅) ≤
(deg‘𝐺) ↔
if((deg‘𝑅) ≤
(deg‘𝑇),
(deg‘𝑇),
(deg‘𝑅)) ≤
(deg‘𝐺))) |
49 | 47, 48 | ifboth 4453 |
. . . . . . . . . . . . 13
⊢
(((deg‘𝑇) ≤
(deg‘𝐺) ∧
(deg‘𝑅) ≤
(deg‘𝐺)) →
if((deg‘𝑅) ≤
(deg‘𝑇),
(deg‘𝑇),
(deg‘𝑅)) ≤
(deg‘𝐺)) |
50 | 40, 46, 49 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((deg‘𝑅) ≤ (deg‘𝑇), (deg‘𝑇), (deg‘𝑅)) ≤ (deg‘𝐺)) |
51 | 20, 27, 30, 34, 50 | letrd 10875 |
. . . . . . . . . . 11
⊢ (𝜑 → (deg‘(𝑅 ∘f −
𝑇)) ≤ (deg‘𝐺)) |
52 | 51 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (deg‘(𝑅
∘f − 𝑇)) ≤ (deg‘𝐺)) |
53 | 13, 2, 3, 4, 6 | plysub 24968 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑝 ∘f − 𝑞) ∈ (Poly‘𝑆)) |
54 | | dgrcl 24982 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∘f −
𝑞) ∈ (Poly‘𝑆) → (deg‘(𝑝 ∘f −
𝑞)) ∈
ℕ0) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘(𝑝 ∘f −
𝑞)) ∈
ℕ0) |
56 | | nn0addge1 12022 |
. . . . . . . . . . . . 13
⊢
(((deg‘𝐺)
∈ ℝ ∧ (deg‘(𝑝 ∘f − 𝑞)) ∈ ℕ0)
→ (deg‘𝐺) ≤
((deg‘𝐺) +
(deg‘(𝑝
∘f − 𝑞)))) |
57 | 30, 55, 56 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐺) ≤ ((deg‘𝐺) + (deg‘(𝑝 ∘f −
𝑞)))) |
58 | 57 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (deg‘𝐺) ≤
((deg‘𝐺) +
(deg‘(𝑝
∘f − 𝑞)))) |
59 | | plyf 24947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
60 | 7, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
61 | 60 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝐹‘𝑧) ∈ ℂ) |
62 | 8, 2, 3, 4 | plymul 24967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 ∘f · 𝑞) ∈ (Poly‘𝑆)) |
63 | | plyf 24947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∘f ·
𝑞) ∈ (Poly‘𝑆) → (𝐺 ∘f · 𝑞):ℂ⟶ℂ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ∘f · 𝑞):ℂ⟶ℂ) |
65 | 64 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝐺 ∘f · 𝑞)‘𝑧) ∈ ℂ) |
66 | 8, 13, 3, 4 | plymul 24967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 ∘f · 𝑝) ∈ (Poly‘𝑆)) |
67 | | plyf 24947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∘f ·
𝑝) ∈ (Poly‘𝑆) → (𝐺 ∘f · 𝑝):ℂ⟶ℂ) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ∘f · 𝑝):ℂ⟶ℂ) |
69 | 68 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝐺 ∘f · 𝑝)‘𝑧) ∈ ℂ) |
70 | 61, 65, 69 | nnncan1d 11109 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (((𝐹‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧)) − ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑝)‘𝑧))) = (((𝐺 ∘f · 𝑝)‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧))) |
71 | 70 | mpteq2dva 5125 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (((𝐹‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧)) − ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑝)‘𝑧)))) = (𝑧 ∈ ℂ ↦ (((𝐺 ∘f · 𝑝)‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧)))) |
72 | | cnex 10696 |
. . . . . . . . . . . . . . . . . 18
⊢ ℂ
∈ V |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℂ ∈
V) |
74 | 61, 65 | subcld 11075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧)) ∈ ℂ) |
75 | 61, 69 | subcld 11075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑝)‘𝑧)) ∈ ℂ) |
76 | 60 | feqmptd 6737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ (𝐹‘𝑧))) |
77 | 64 | feqmptd 6737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ∘f · 𝑞) = (𝑧 ∈ ℂ ↦ ((𝐺 ∘f · 𝑞)‘𝑧))) |
78 | 73, 61, 65, 76, 77 | offval2 7444 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 ∘f − (𝐺 ∘f ·
𝑞)) = (𝑧 ∈ ℂ ↦ ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧)))) |
79 | 10, 78 | syl5eq 2785 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 = (𝑧 ∈ ℂ ↦ ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧)))) |
80 | 68 | feqmptd 6737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ∘f · 𝑝) = (𝑧 ∈ ℂ ↦ ((𝐺 ∘f · 𝑝)‘𝑧))) |
81 | 73, 61, 69, 76, 80 | offval2 7444 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 ∘f − (𝐺 ∘f ·
𝑝)) = (𝑧 ∈ ℂ ↦ ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑝)‘𝑧)))) |
82 | 14, 81 | syl5eq 2785 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 = (𝑧 ∈ ℂ ↦ ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑝)‘𝑧)))) |
83 | 73, 74, 75, 79, 82 | offval2 7444 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑅 ∘f − 𝑇) = (𝑧 ∈ ℂ ↦ (((𝐹‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧)) − ((𝐹‘𝑧) − ((𝐺 ∘f · 𝑝)‘𝑧))))) |
84 | 73, 69, 65, 80, 77 | offval2 7444 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐺 ∘f · 𝑝) ∘f −
(𝐺 ∘f
· 𝑞)) = (𝑧 ∈ ℂ ↦ (((𝐺 ∘f ·
𝑝)‘𝑧) − ((𝐺 ∘f · 𝑞)‘𝑧)))) |
85 | 71, 83, 84 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅 ∘f − 𝑇) = ((𝐺 ∘f · 𝑝) ∘f −
(𝐺 ∘f
· 𝑞))) |
86 | | plyf 24947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ) |
87 | 8, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:ℂ⟶ℂ) |
88 | | plyf 24947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ (Poly‘𝑆) → 𝑝:ℂ⟶ℂ) |
89 | 13, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑝:ℂ⟶ℂ) |
90 | | plyf 24947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ (Poly‘𝑆) → 𝑞:ℂ⟶ℂ) |
91 | 2, 90 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑞:ℂ⟶ℂ) |
92 | | subdi 11151 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 · (𝑦 − 𝑧)) = ((𝑥 · 𝑦) − (𝑥 · 𝑧))) |
93 | 92 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑥 · (𝑦 − 𝑧)) = ((𝑥 · 𝑦) − (𝑥 · 𝑧))) |
94 | 73, 87, 89, 91, 93 | caofdi 7463 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 ∘f · (𝑝 ∘f −
𝑞)) = ((𝐺 ∘f · 𝑝) ∘f −
(𝐺 ∘f
· 𝑞))) |
95 | 85, 94 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 ∘f − 𝑇) = (𝐺 ∘f · (𝑝 ∘f −
𝑞))) |
96 | 95 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘(𝑅 ∘f −
𝑇)) = (deg‘(𝐺 ∘f ·
(𝑝 ∘f
− 𝑞)))) |
97 | 96 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (deg‘(𝑅
∘f − 𝑇)) = (deg‘(𝐺 ∘f · (𝑝 ∘f −
𝑞)))) |
98 | 8 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ 𝐺 ∈
(Poly‘𝑆)) |
99 | 9 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ 𝐺 ≠
0𝑝) |
100 | 53 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (𝑝
∘f − 𝑞) ∈ (Poly‘𝑆)) |
101 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (𝑝
∘f − 𝑞) ≠
0𝑝) |
102 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(deg‘𝐺) =
(deg‘𝐺) |
103 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(deg‘(𝑝
∘f − 𝑞)) = (deg‘(𝑝 ∘f − 𝑞)) |
104 | 102, 103 | dgrmul 25019 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) ∧ ((𝑝 ∘f −
𝑞) ∈ (Poly‘𝑆) ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝))
→ (deg‘(𝐺
∘f · (𝑝 ∘f − 𝑞))) = ((deg‘𝐺) + (deg‘(𝑝 ∘f −
𝑞)))) |
105 | 98, 99, 100, 101, 104 | syl22anc 838 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (deg‘(𝐺
∘f · (𝑝 ∘f − 𝑞))) = ((deg‘𝐺) + (deg‘(𝑝 ∘f −
𝑞)))) |
106 | 97, 105 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (deg‘(𝑅
∘f − 𝑇)) = ((deg‘𝐺) + (deg‘(𝑝 ∘f − 𝑞)))) |
107 | 58, 106 | breqtrrd 5058 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (deg‘𝐺) ≤
(deg‘(𝑅
∘f − 𝑇))) |
108 | 20, 30 | letri3d 10860 |
. . . . . . . . . . 11
⊢ (𝜑 → ((deg‘(𝑅 ∘f −
𝑇)) = (deg‘𝐺) ↔ ((deg‘(𝑅 ∘f −
𝑇)) ≤ (deg‘𝐺) ∧ (deg‘𝐺) ≤ (deg‘(𝑅 ∘f −
𝑇))))) |
109 | 108 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ ((deg‘(𝑅
∘f − 𝑇)) = (deg‘𝐺) ↔ ((deg‘(𝑅 ∘f − 𝑇)) ≤ (deg‘𝐺) ∧ (deg‘𝐺) ≤ (deg‘(𝑅 ∘f −
𝑇))))) |
110 | 52, 107, 109 | mpbir2and 713 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (deg‘(𝑅
∘f − 𝑇)) = (deg‘𝐺)) |
111 | 110 | fveq2d 6678 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ ((coeff‘(𝑅
∘f − 𝑇))‘(deg‘(𝑅 ∘f − 𝑇))) = ((coeff‘(𝑅 ∘f −
𝑇))‘(deg‘𝐺))) |
112 | 42, 36 | coesub 25006 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ (Poly‘𝑆) ∧ 𝑇 ∈ (Poly‘𝑆)) → (coeff‘(𝑅 ∘f − 𝑇)) = ((coeff‘𝑅) ∘f −
(coeff‘𝑇))) |
113 | 12, 16, 112 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (coeff‘(𝑅 ∘f −
𝑇)) = ((coeff‘𝑅) ∘f −
(coeff‘𝑇))) |
114 | 113 | fveq1d 6676 |
. . . . . . . . . . 11
⊢ (𝜑 → ((coeff‘(𝑅 ∘f −
𝑇))‘(deg‘𝐺)) = (((coeff‘𝑅) ∘f −
(coeff‘𝑇))‘(deg‘𝐺))) |
115 | 42 | coef3 24981 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ (Poly‘𝑆) → (coeff‘𝑅):ℕ0⟶ℂ) |
116 | | ffn 6504 |
. . . . . . . . . . . . . 14
⊢
((coeff‘𝑅):ℕ0⟶ℂ →
(coeff‘𝑅) Fn
ℕ0) |
117 | 12, 115, 116 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (coeff‘𝑅) Fn
ℕ0) |
118 | 36 | coef3 24981 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ (Poly‘𝑆) → (coeff‘𝑇):ℕ0⟶ℂ) |
119 | | ffn 6504 |
. . . . . . . . . . . . . 14
⊢
((coeff‘𝑇):ℕ0⟶ℂ →
(coeff‘𝑇) Fn
ℕ0) |
120 | 16, 118, 119 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (coeff‘𝑇) Fn
ℕ0) |
121 | | nn0ex 11982 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V |
122 | 121 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ0 ∈
V) |
123 | | inidm 4109 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
124 | 45 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((coeff‘𝑅)‘(deg‘𝐺)) = 0) |
125 | 124 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (deg‘𝐺) ∈ ℕ0)
→ ((coeff‘𝑅)‘(deg‘𝐺)) = 0) |
126 | 39 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((coeff‘𝑇)‘(deg‘𝐺)) = 0) |
127 | 126 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (deg‘𝐺) ∈ ℕ0)
→ ((coeff‘𝑇)‘(deg‘𝐺)) = 0) |
128 | 117, 120,
122, 122, 123, 125, 127 | ofval 7435 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (deg‘𝐺) ∈ ℕ0)
→ (((coeff‘𝑅)
∘f − (coeff‘𝑇))‘(deg‘𝐺)) = (0 − 0)) |
129 | 29, 128 | mpdan 687 |
. . . . . . . . . . 11
⊢ (𝜑 → (((coeff‘𝑅) ∘f −
(coeff‘𝑇))‘(deg‘𝐺)) = (0 − 0)) |
130 | 114, 129 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (𝜑 → ((coeff‘(𝑅 ∘f −
𝑇))‘(deg‘𝐺)) = (0 −
0)) |
131 | | 0m0e0 11836 |
. . . . . . . . . 10
⊢ (0
− 0) = 0 |
132 | 130, 131 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝜑 → ((coeff‘(𝑅 ∘f −
𝑇))‘(deg‘𝐺)) = 0) |
133 | 132 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ ((coeff‘(𝑅
∘f − 𝑇))‘(deg‘𝐺)) = 0) |
134 | 111, 133 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ ((coeff‘(𝑅
∘f − 𝑇))‘(deg‘(𝑅 ∘f − 𝑇))) = 0) |
135 | | eqid 2738 |
. . . . . . . . . 10
⊢
(deg‘(𝑅
∘f − 𝑇)) = (deg‘(𝑅 ∘f − 𝑇)) |
136 | | eqid 2738 |
. . . . . . . . . 10
⊢
(coeff‘(𝑅
∘f − 𝑇)) = (coeff‘(𝑅 ∘f − 𝑇)) |
137 | 135, 136 | dgreq0 25014 |
. . . . . . . . 9
⊢ ((𝑅 ∘f −
𝑇) ∈ (Poly‘𝑆) → ((𝑅 ∘f − 𝑇) = 0𝑝 ↔
((coeff‘(𝑅
∘f − 𝑇))‘(deg‘(𝑅 ∘f − 𝑇))) = 0)) |
138 | 17, 137 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝑅 ∘f − 𝑇) = 0𝑝 ↔
((coeff‘(𝑅
∘f − 𝑇))‘(deg‘(𝑅 ∘f − 𝑇))) = 0)) |
139 | 138 | biimpar 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ((coeff‘(𝑅 ∘f −
𝑇))‘(deg‘(𝑅 ∘f −
𝑇))) = 0) → (𝑅 ∘f −
𝑇) =
0𝑝) |
140 | 134, 139 | syldan 594 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∘f − 𝑞) ≠ 0𝑝)
→ (𝑅
∘f − 𝑇) = 0𝑝) |
141 | 140 | ex 416 |
. . . . 5
⊢ (𝜑 → ((𝑝 ∘f − 𝑞) ≠ 0𝑝
→ (𝑅
∘f − 𝑇) = 0𝑝)) |
142 | | plymul0or 25029 |
. . . . . . 7
⊢ ((𝐺 ∈ (Poly‘𝑆) ∧ (𝑝 ∘f − 𝑞) ∈ (Poly‘𝑆)) → ((𝐺 ∘f · (𝑝 ∘f −
𝑞)) = 0𝑝
↔ (𝐺 =
0𝑝 ∨ (𝑝 ∘f − 𝑞) =
0𝑝))) |
143 | 8, 53, 142 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((𝐺 ∘f · (𝑝 ∘f −
𝑞)) = 0𝑝
↔ (𝐺 =
0𝑝 ∨ (𝑝 ∘f − 𝑞) =
0𝑝))) |
144 | 95 | eqeq1d 2740 |
. . . . . 6
⊢ (𝜑 → ((𝑅 ∘f − 𝑇) = 0𝑝 ↔
(𝐺 ∘f
· (𝑝
∘f − 𝑞)) = 0𝑝)) |
145 | 9 | neneqd 2939 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐺 = 0𝑝) |
146 | | biorf 936 |
. . . . . . 7
⊢ (¬
𝐺 = 0𝑝
→ ((𝑝
∘f − 𝑞) = 0𝑝 ↔ (𝐺 = 0𝑝 ∨
(𝑝 ∘f
− 𝑞) =
0𝑝))) |
147 | 145, 146 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑝 ∘f − 𝑞) = 0𝑝 ↔
(𝐺 = 0𝑝
∨ (𝑝 ∘f
− 𝑞) =
0𝑝))) |
148 | 143, 144,
147 | 3bitr4d 314 |
. . . . 5
⊢ (𝜑 → ((𝑅 ∘f − 𝑇) = 0𝑝 ↔
(𝑝 ∘f
− 𝑞) =
0𝑝)) |
149 | 141, 148 | sylibd 242 |
. . . 4
⊢ (𝜑 → ((𝑝 ∘f − 𝑞) ≠ 0𝑝
→ (𝑝
∘f − 𝑞) = 0𝑝)) |
150 | 1, 149 | pm2.61dne 3020 |
. . 3
⊢ (𝜑 → (𝑝 ∘f − 𝑞) =
0𝑝) |
151 | | df-0p 24422 |
. . 3
⊢
0𝑝 = (ℂ × {0}) |
152 | 150, 151 | eqtrdi 2789 |
. 2
⊢ (𝜑 → (𝑝 ∘f − 𝑞) = (ℂ ×
{0})) |
153 | | ofsubeq0 11713 |
. . 3
⊢ ((ℂ
∈ V ∧ 𝑝:ℂ⟶ℂ ∧ 𝑞:ℂ⟶ℂ) →
((𝑝 ∘f
− 𝑞) = (ℂ
× {0}) ↔ 𝑝 =
𝑞)) |
154 | 72, 89, 91, 153 | mp3an2i 1467 |
. 2
⊢ (𝜑 → ((𝑝 ∘f − 𝑞) = (ℂ × {0}) ↔
𝑝 = 𝑞)) |
155 | 152, 154 | mpbid 235 |
1
⊢ (𝜑 → 𝑝 = 𝑞) |