Proof of Theorem dgrmul
Step | Hyp | Ref
| Expression |
1 | | dgradd.1 |
. . . 4
⊢ 𝑀 = (deg‘𝐹) |
2 | | dgradd.2 |
. . . 4
⊢ 𝑁 = (deg‘𝐺) |
3 | 1, 2 | dgrmul2 25426 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘f · 𝐺)) ≤ (𝑀 + 𝑁)) |
4 | 3 | ad2ant2r 744 |
. 2
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
(deg‘(𝐹
∘f · 𝐺)) ≤ (𝑀 + 𝑁)) |
5 | | plymulcl 25378 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f · 𝐺) ∈
(Poly‘ℂ)) |
6 | 5 | ad2ant2r 744 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) → (𝐹 ∘f ·
𝐺) ∈
(Poly‘ℂ)) |
7 | | dgrcl 25390 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
8 | 1, 7 | eqeltrid 2845 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑀 ∈
ℕ0) |
9 | 8 | ad2antrr 723 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) → 𝑀 ∈
ℕ0) |
10 | | dgrcl 25390 |
. . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
11 | 2, 10 | eqeltrid 2845 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) |
12 | 11 | ad2antrl 725 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) → 𝑁 ∈
ℕ0) |
13 | 9, 12 | nn0addcld 12295 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) → (𝑀 + 𝑁) ∈
ℕ0) |
14 | | eqid 2740 |
. . . . . 6
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
15 | | eqid 2740 |
. . . . . 6
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
16 | 14, 15, 1, 2 | coemulhi 25411 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘f · 𝐺))‘(𝑀 + 𝑁)) = (((coeff‘𝐹)‘𝑀) · ((coeff‘𝐺)‘𝑁))) |
17 | 16 | ad2ant2r 744 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
((coeff‘(𝐹
∘f · 𝐺))‘(𝑀 + 𝑁)) = (((coeff‘𝐹)‘𝑀) · ((coeff‘𝐺)‘𝑁))) |
18 | 14 | coef3 25389 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
19 | 18 | ad2antrr 723 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
(coeff‘𝐹):ℕ0⟶ℂ) |
20 | 19, 9 | ffvelrnd 6957 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
((coeff‘𝐹)‘𝑀) ∈ ℂ) |
21 | 15 | coef3 25389 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (coeff‘𝐺):ℕ0⟶ℂ) |
22 | 21 | ad2antrl 725 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
(coeff‘𝐺):ℕ0⟶ℂ) |
23 | 22, 12 | ffvelrnd 6957 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
((coeff‘𝐺)‘𝑁) ∈ ℂ) |
24 | 1, 14 | dgreq0 25422 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔
((coeff‘𝐹)‘𝑀) = 0)) |
25 | 24 | necon3bid 2990 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 ≠ 0𝑝 ↔
((coeff‘𝐹)‘𝑀) ≠ 0)) |
26 | 25 | biimpa 477 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) →
((coeff‘𝐹)‘𝑀) ≠ 0) |
27 | 26 | adantr 481 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
((coeff‘𝐹)‘𝑀) ≠ 0) |
28 | 2, 15 | dgreq0 25422 |
. . . . . . . 8
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘𝑁) = 0)) |
29 | 28 | necon3bid 2990 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐺 ≠ 0𝑝 ↔
((coeff‘𝐺)‘𝑁) ≠ 0)) |
30 | 29 | biimpa 477 |
. . . . . 6
⊢ ((𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) →
((coeff‘𝐺)‘𝑁) ≠ 0) |
31 | 30 | adantl 482 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
((coeff‘𝐺)‘𝑁) ≠ 0) |
32 | 20, 23, 27, 31 | mulne0d 11625 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
(((coeff‘𝐹)‘𝑀) · ((coeff‘𝐺)‘𝑁)) ≠ 0) |
33 | 17, 32 | eqnetrd 3013 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
((coeff‘(𝐹
∘f · 𝐺))‘(𝑀 + 𝑁)) ≠ 0) |
34 | | eqid 2740 |
. . . 4
⊢
(coeff‘(𝐹
∘f · 𝐺)) = (coeff‘(𝐹 ∘f · 𝐺)) |
35 | | eqid 2740 |
. . . 4
⊢
(deg‘(𝐹
∘f · 𝐺)) = (deg‘(𝐹 ∘f · 𝐺)) |
36 | 34, 35 | dgrub 25391 |
. . 3
⊢ (((𝐹 ∘f ·
𝐺) ∈
(Poly‘ℂ) ∧ (𝑀 + 𝑁) ∈ ℕ0 ∧
((coeff‘(𝐹
∘f · 𝐺))‘(𝑀 + 𝑁)) ≠ 0) → (𝑀 + 𝑁) ≤ (deg‘(𝐹 ∘f · 𝐺))) |
37 | 6, 13, 33, 36 | syl3anc 1370 |
. 2
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) → (𝑀 + 𝑁) ≤ (deg‘(𝐹 ∘f · 𝐺))) |
38 | | dgrcl 25390 |
. . . . 5
⊢ ((𝐹 ∘f ·
𝐺) ∈
(Poly‘ℂ) → (deg‘(𝐹 ∘f · 𝐺)) ∈
ℕ0) |
39 | 6, 38 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
(deg‘(𝐹
∘f · 𝐺)) ∈
ℕ0) |
40 | 39 | nn0red 12292 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
(deg‘(𝐹
∘f · 𝐺)) ∈ ℝ) |
41 | 13 | nn0red 12292 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) → (𝑀 + 𝑁) ∈ ℝ) |
42 | 40, 41 | letri3d 11115 |
. 2
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
((deg‘(𝐹
∘f · 𝐺)) = (𝑀 + 𝑁) ↔ ((deg‘(𝐹 ∘f · 𝐺)) ≤ (𝑀 + 𝑁) ∧ (𝑀 + 𝑁) ≤ (deg‘(𝐹 ∘f · 𝐺))))) |
43 | 4, 37, 42 | mpbir2and 710 |
1
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
(deg‘(𝐹
∘f · 𝐺)) = (𝑀 + 𝑁)) |