Step | Hyp | Ref
| Expression |
1 | | dgrcl 24994 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
2 | | dgrcl 24994 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
3 | | nn0addcl 12023 |
. . . . . . 7
⊢
(((deg‘𝐹)
∈ ℕ0 ∧ (deg‘𝐺) ∈ ℕ0) →
((deg‘𝐹) +
(deg‘𝐺)) ∈
ℕ0) |
4 | 1, 2, 3 | syl2an 599 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((deg‘𝐹) + (deg‘𝐺)) ∈
ℕ0) |
5 | | c0ex 10725 |
. . . . . . 7
⊢ 0 ∈
V |
6 | 5 | fvconst2 6988 |
. . . . . 6
⊢
(((deg‘𝐹) +
(deg‘𝐺)) ∈
ℕ0 → ((ℕ0 ×
{0})‘((deg‘𝐹) +
(deg‘𝐺))) =
0) |
7 | 4, 6 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((ℕ0 ×
{0})‘((deg‘𝐹) +
(deg‘𝐺))) =
0) |
8 | | fveq2 6686 |
. . . . . . . 8
⊢ ((𝐹 ∘f ·
𝐺) = 0𝑝
→ (coeff‘(𝐹
∘f · 𝐺)) =
(coeff‘0𝑝)) |
9 | | coe0 25017 |
. . . . . . . 8
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
10 | 8, 9 | eqtrdi 2790 |
. . . . . . 7
⊢ ((𝐹 ∘f ·
𝐺) = 0𝑝
→ (coeff‘(𝐹
∘f · 𝐺)) = (ℕ0 ×
{0})) |
11 | 10 | fveq1d 6688 |
. . . . . 6
⊢ ((𝐹 ∘f ·
𝐺) = 0𝑝
→ ((coeff‘(𝐹
∘f · 𝐺))‘((deg‘𝐹) + (deg‘𝐺))) = ((ℕ0 ×
{0})‘((deg‘𝐹) +
(deg‘𝐺)))) |
12 | 11 | eqeq1d 2741 |
. . . . 5
⊢ ((𝐹 ∘f ·
𝐺) = 0𝑝
→ (((coeff‘(𝐹
∘f · 𝐺))‘((deg‘𝐹) + (deg‘𝐺))) = 0 ↔ ((ℕ0 ×
{0})‘((deg‘𝐹) +
(deg‘𝐺))) =
0)) |
13 | 7, 12 | syl5ibrcom 250 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐹 ∘f · 𝐺) = 0𝑝 →
((coeff‘(𝐹
∘f · 𝐺))‘((deg‘𝐹) + (deg‘𝐺))) = 0)) |
14 | | eqid 2739 |
. . . . . . 7
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
15 | | eqid 2739 |
. . . . . . 7
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
16 | | eqid 2739 |
. . . . . . 7
⊢
(deg‘𝐹) =
(deg‘𝐹) |
17 | | eqid 2739 |
. . . . . . 7
⊢
(deg‘𝐺) =
(deg‘𝐺) |
18 | 14, 15, 16, 17 | coemulhi 25015 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘f · 𝐺))‘((deg‘𝐹) + (deg‘𝐺))) = (((coeff‘𝐹)‘(deg‘𝐹)) · ((coeff‘𝐺)‘(deg‘𝐺)))) |
19 | 18 | eqeq1d 2741 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (((coeff‘(𝐹 ∘f · 𝐺))‘((deg‘𝐹) + (deg‘𝐺))) = 0 ↔ (((coeff‘𝐹)‘(deg‘𝐹)) · ((coeff‘𝐺)‘(deg‘𝐺))) = 0)) |
20 | 14 | coef3 24993 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
21 | 20 | adantr 484 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘𝐹):ℕ0⟶ℂ) |
22 | 1 | adantr 484 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈
ℕ0) |
23 | 21, 22 | ffvelrnd 6874 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘𝐹)‘(deg‘𝐹)) ∈ ℂ) |
24 | 15 | coef3 24993 |
. . . . . . . 8
⊢ (𝐺 ∈ (Poly‘𝑆) → (coeff‘𝐺):ℕ0⟶ℂ) |
25 | 24 | adantl 485 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘𝐺):ℕ0⟶ℂ) |
26 | 2 | adantl 485 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘𝐺) ∈
ℕ0) |
27 | 25, 26 | ffvelrnd 6874 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘𝐺)‘(deg‘𝐺)) ∈ ℂ) |
28 | 23, 27 | mul0ord 11380 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((((coeff‘𝐹)‘(deg‘𝐹)) · ((coeff‘𝐺)‘(deg‘𝐺))) = 0 ↔ (((coeff‘𝐹)‘(deg‘𝐹)) = 0 ∨ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))) |
29 | 19, 28 | bitrd 282 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (((coeff‘(𝐹 ∘f · 𝐺))‘((deg‘𝐹) + (deg‘𝐺))) = 0 ↔ (((coeff‘𝐹)‘(deg‘𝐹)) = 0 ∨ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))) |
30 | 13, 29 | sylibd 242 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐹 ∘f · 𝐺) = 0𝑝 →
(((coeff‘𝐹)‘(deg‘𝐹)) = 0 ∨ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))) |
31 | 16, 14 | dgreq0 25026 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔
((coeff‘𝐹)‘(deg‘𝐹)) = 0)) |
32 | 31 | adantr 484 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 = 0𝑝 ↔
((coeff‘𝐹)‘(deg‘𝐹)) = 0)) |
33 | 17, 15 | dgreq0 25026 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘(deg‘𝐺)) = 0)) |
34 | 33 | adantl 485 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘(deg‘𝐺)) = 0)) |
35 | 32, 34 | orbi12d 918 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐹 = 0𝑝 ∨ 𝐺 = 0𝑝) ↔
(((coeff‘𝐹)‘(deg‘𝐹)) = 0 ∨ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))) |
36 | 30, 35 | sylibrd 262 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐹 ∘f · 𝐺) = 0𝑝 →
(𝐹 = 0𝑝
∨ 𝐺 =
0𝑝))) |
37 | | cnex 10708 |
. . . . . . 7
⊢ ℂ
∈ V |
38 | 37 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ℂ ∈ V) |
39 | | plyf 24959 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ) |
40 | 39 | adantl 485 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐺:ℂ⟶ℂ) |
41 | | 0cnd 10724 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 0 ∈ ℂ) |
42 | | mul02 10908 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → (0
· 𝑥) =
0) |
43 | 42 | adantl 485 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0) |
44 | 38, 40, 41, 41, 43 | caofid2 7470 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((ℂ × {0})
∘f · 𝐺) = (ℂ × {0})) |
45 | | id 22 |
. . . . . . . 8
⊢ (𝐹 = 0𝑝 →
𝐹 =
0𝑝) |
46 | | df-0p 24434 |
. . . . . . . 8
⊢
0𝑝 = (ℂ × {0}) |
47 | 45, 46 | eqtrdi 2790 |
. . . . . . 7
⊢ (𝐹 = 0𝑝 →
𝐹 = (ℂ ×
{0})) |
48 | 47 | oveq1d 7197 |
. . . . . 6
⊢ (𝐹 = 0𝑝 →
(𝐹 ∘f
· 𝐺) = ((ℂ
× {0}) ∘f · 𝐺)) |
49 | 48 | eqeq1d 2741 |
. . . . 5
⊢ (𝐹 = 0𝑝 →
((𝐹 ∘f
· 𝐺) = (ℂ
× {0}) ↔ ((ℂ × {0}) ∘f · 𝐺) = (ℂ ×
{0}))) |
50 | 44, 49 | syl5ibrcom 250 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 = 0𝑝 → (𝐹 ∘f ·
𝐺) = (ℂ ×
{0}))) |
51 | | plyf 24959 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
52 | 51 | adantr 484 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ) |
53 | | mul01 10909 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → (𝑥 · 0) =
0) |
54 | 53 | adantl 485 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑥 ∈ ℂ) → (𝑥 · 0) = 0) |
55 | 38, 52, 41, 41, 54 | caofid1 7469 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f · (ℂ
× {0})) = (ℂ × {0})) |
56 | | id 22 |
. . . . . . . 8
⊢ (𝐺 = 0𝑝 →
𝐺 =
0𝑝) |
57 | 56, 46 | eqtrdi 2790 |
. . . . . . 7
⊢ (𝐺 = 0𝑝 →
𝐺 = (ℂ ×
{0})) |
58 | 57 | oveq2d 7198 |
. . . . . 6
⊢ (𝐺 = 0𝑝 →
(𝐹 ∘f
· 𝐺) = (𝐹 ∘f ·
(ℂ × {0}))) |
59 | 58 | eqeq1d 2741 |
. . . . 5
⊢ (𝐺 = 0𝑝 →
((𝐹 ∘f
· 𝐺) = (ℂ
× {0}) ↔ (𝐹
∘f · (ℂ × {0})) = (ℂ ×
{0}))) |
60 | 55, 59 | syl5ibrcom 250 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐺 = 0𝑝 → (𝐹 ∘f ·
𝐺) = (ℂ ×
{0}))) |
61 | 50, 60 | jaod 858 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐹 = 0𝑝 ∨ 𝐺 = 0𝑝) →
(𝐹 ∘f
· 𝐺) = (ℂ
× {0}))) |
62 | 46 | eqeq2i 2752 |
. . 3
⊢ ((𝐹 ∘f ·
𝐺) = 0𝑝
↔ (𝐹
∘f · 𝐺) = (ℂ × {0})) |
63 | 61, 62 | syl6ibr 255 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐹 = 0𝑝 ∨ 𝐺 = 0𝑝) →
(𝐹 ∘f
· 𝐺) =
0𝑝)) |
64 | 36, 63 | impbid 215 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐹 ∘f · 𝐺) = 0𝑝 ↔
(𝐹 = 0𝑝
∨ 𝐺 =
0𝑝))) |