Step | Hyp | Ref
| Expression |
1 | | qsscn 12556 |
. . . . . 6
⊢ ℚ
⊆ ℂ |
2 | | eldifi 4041 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝}) → 𝑎 ∈
(Poly‘ℚ)) |
3 | 2 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → 𝑎 ∈
(Poly‘ℚ)) |
4 | | zssq 12552 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℚ |
5 | | 0z 12187 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
6 | 4, 5 | sselii 3897 |
. . . . . . . . 9
⊢ 0 ∈
ℚ |
7 | | eqid 2737 |
. . . . . . . . . 10
⊢
(coeff‘𝑎) =
(coeff‘𝑎) |
8 | 7 | coef2 25125 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (Poly‘ℚ)
∧ 0 ∈ ℚ) → (coeff‘𝑎):ℕ0⟶ℚ) |
9 | 3, 6, 8 | sylancl 589 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (coeff‘𝑎):ℕ0⟶ℚ) |
10 | | dgrcl 25127 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Poly‘ℚ)
→ (deg‘𝑎) ∈
ℕ0) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (deg‘𝑎) ∈
ℕ0) |
12 | 9, 11 | ffvelrnd 6905 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘𝑎)‘(deg‘𝑎)) ∈
ℚ) |
13 | | eldifsni 4703 |
. . . . . . . . 9
⊢ (𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝}) → 𝑎 ≠ 0𝑝) |
14 | 13 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → 𝑎 ≠ 0𝑝) |
15 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(deg‘𝑎) =
(deg‘𝑎) |
16 | 15, 7 | dgreq0 25159 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (Poly‘ℚ)
→ (𝑎 =
0𝑝 ↔ ((coeff‘𝑎)‘(deg‘𝑎)) = 0)) |
17 | 16 | necon3bid 2985 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Poly‘ℚ)
→ (𝑎 ≠
0𝑝 ↔ ((coeff‘𝑎)‘(deg‘𝑎)) ≠ 0)) |
18 | 3, 17 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (𝑎 ≠ 0𝑝 ↔
((coeff‘𝑎)‘(deg‘𝑎)) ≠ 0)) |
19 | 14, 18 | mpbid 235 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘𝑎)‘(deg‘𝑎)) ≠ 0) |
20 | | qreccl 12565 |
. . . . . . 7
⊢
((((coeff‘𝑎)‘(deg‘𝑎)) ∈ ℚ ∧ ((coeff‘𝑎)‘(deg‘𝑎)) ≠ 0) → (1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ ℚ) |
21 | 12, 19, 20 | syl2anc 587 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (1 / ((coeff‘𝑎)‘(deg‘𝑎))) ∈
ℚ) |
22 | | plyconst 25100 |
. . . . . 6
⊢ ((ℚ
⊆ ℂ ∧ (1 / ((coeff‘𝑎)‘(deg‘𝑎))) ∈ ℚ) → (ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈
(Poly‘ℚ)) |
23 | 1, 21, 22 | sylancr 590 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∈
(Poly‘ℚ)) |
24 | | simpl 486 |
. . . . . 6
⊢
(((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
→ (ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈
(Poly‘ℚ)) |
25 | | simpr 488 |
. . . . . 6
⊢
(((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
→ 𝑎 ∈
(Poly‘ℚ)) |
26 | | qaddcl 12561 |
. . . . . . 7
⊢ ((𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ) → (𝑏 + 𝑐) ∈ ℚ) |
27 | 26 | adantl 485 |
. . . . . 6
⊢
((((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
∧ (𝑏 ∈ ℚ
∧ 𝑐 ∈ ℚ))
→ (𝑏 + 𝑐) ∈
ℚ) |
28 | | qmulcl 12563 |
. . . . . . 7
⊢ ((𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ) → (𝑏 · 𝑐) ∈ ℚ) |
29 | 28 | adantl 485 |
. . . . . 6
⊢
((((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
∧ (𝑏 ∈ ℚ
∧ 𝑐 ∈ ℚ))
→ (𝑏 · 𝑐) ∈
ℚ) |
30 | 24, 25, 27, 29 | plymul 25112 |
. . . . 5
⊢
(((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
→ ((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) ∈
(Poly‘ℚ)) |
31 | 23, 3, 30 | syl2anc 587 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) ∈
(Poly‘ℚ)) |
32 | 7 | coef3 25126 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Poly‘ℚ)
→ (coeff‘𝑎):ℕ0⟶ℂ) |
33 | 3, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (coeff‘𝑎):ℕ0⟶ℂ) |
34 | 33, 11 | ffvelrnd 6905 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘𝑎)‘(deg‘𝑎)) ∈
ℂ) |
35 | 34, 19 | reccld 11601 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (1 / ((coeff‘𝑎)‘(deg‘𝑎))) ∈
ℂ) |
36 | 34, 19 | recne0d 11602 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (1 / ((coeff‘𝑎)‘(deg‘𝑎))) ≠ 0) |
37 | | dgrmulc 25165 |
. . . . . 6
⊢ (((1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ ℂ ∧ (1 /
((coeff‘𝑎)‘(deg‘𝑎))) ≠ 0 ∧ 𝑎 ∈ (Poly‘ℚ)) →
(deg‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)) = (deg‘𝑎)) |
38 | 35, 36, 3, 37 | syl3anc 1373 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (deg‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)) = (deg‘𝑎)) |
39 | | simprl 771 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (deg‘𝑎) = (degAA‘𝐴)) |
40 | 38, 39 | eqtrd 2777 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (deg‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)) =
(degAA‘𝐴)) |
41 | | aacn 25210 |
. . . . . . 7
⊢ (𝐴 ∈ 𝔸 → 𝐴 ∈
ℂ) |
42 | 41 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → 𝐴 ∈ ℂ) |
43 | | ovex 7246 |
. . . . . . . 8
⊢ (1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ V |
44 | | fnconstg 6607 |
. . . . . . . 8
⊢ ((1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ V → (ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) Fn ℂ) |
45 | 43, 44 | mp1i 13 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) Fn ℂ) |
46 | | plyf 25092 |
. . . . . . . 8
⊢ (𝑎 ∈ (Poly‘ℚ)
→ 𝑎:ℂ⟶ℂ) |
47 | | ffn 6545 |
. . . . . . . 8
⊢ (𝑎:ℂ⟶ℂ →
𝑎 Fn
ℂ) |
48 | 3, 46, 47 | 3syl 18 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → 𝑎 Fn ℂ) |
49 | | cnex 10810 |
. . . . . . . 8
⊢ ℂ
∈ V |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ℂ ∈
V) |
51 | | inidm 4133 |
. . . . . . 7
⊢ (ℂ
∩ ℂ) = ℂ |
52 | 43 | fvconst2 7019 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))})‘𝐴) = (1 / ((coeff‘𝑎)‘(deg‘𝑎)))) |
53 | 52 | adantl 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → ((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))})‘𝐴) = (1 / ((coeff‘𝑎)‘(deg‘𝑎)))) |
54 | | simplrr 778 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → (𝑎‘𝐴) = 0) |
55 | 45, 48, 50, 50, 51, 53, 54 | ofval 7479 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → (((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)‘𝐴) = ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · 0)) |
56 | 42, 55 | mpdan 687 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)‘𝐴) = ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · 0)) |
57 | 35 | mul01d 11031 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · 0) =
0) |
58 | 56, 57 | eqtrd 2777 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)‘𝐴) = 0) |
59 | | coemulc 25149 |
. . . . . . 7
⊢ (((1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ ℂ ∧ 𝑎 ∈ (Poly‘ℚ)) →
(coeff‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)) = ((ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f ·
(coeff‘𝑎))) |
60 | 35, 3, 59 | syl2anc 587 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)) = ((ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f ·
(coeff‘𝑎))) |
61 | 60 | fveq1d 6719 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎))‘(degAA‘𝐴)) = (((ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f ·
(coeff‘𝑎))‘(degAA‘𝐴))) |
62 | | dgraacl 40674 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝔸 →
(degAA‘𝐴)
∈ ℕ) |
63 | 62 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (degAA‘𝐴) ∈
ℕ) |
64 | 63 | nnnn0d 12150 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (degAA‘𝐴) ∈
ℕ0) |
65 | | fnconstg 6607 |
. . . . . . . 8
⊢ ((1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ V → (ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) Fn
ℕ0) |
66 | 43, 65 | mp1i 13 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (ℕ0 ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) Fn
ℕ0) |
67 | 33 | ffnd 6546 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (coeff‘𝑎) Fn
ℕ0) |
68 | | nn0ex 12096 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
69 | 68 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ℕ0 ∈
V) |
70 | | inidm 4133 |
. . . . . . 7
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
71 | 43 | fvconst2 7019 |
. . . . . . . 8
⊢
((degAA‘𝐴) ∈ ℕ0 →
((ℕ0 × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))})‘(degAA‘𝐴)) = (1 / ((coeff‘𝑎)‘(deg‘𝑎)))) |
72 | 71 | adantl 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ ((ℕ0 × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))})‘(degAA‘𝐴)) = (1 / ((coeff‘𝑎)‘(deg‘𝑎)))) |
73 | | simplrl 777 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ (deg‘𝑎) =
(degAA‘𝐴)) |
74 | 73 | eqcomd 2743 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ (degAA‘𝐴) = (deg‘𝑎)) |
75 | 74 | fveq2d 6721 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ ((coeff‘𝑎)‘(degAA‘𝐴)) = ((coeff‘𝑎)‘(deg‘𝑎))) |
76 | 66, 67, 69, 69, 70, 72, 75 | ofval 7479 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ (((ℕ0 × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f ·
(coeff‘𝑎))‘(degAA‘𝐴)) = ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · ((coeff‘𝑎)‘(deg‘𝑎)))) |
77 | 64, 76 | mpdan 687 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (((ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f ·
(coeff‘𝑎))‘(degAA‘𝐴)) = ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · ((coeff‘𝑎)‘(deg‘𝑎)))) |
78 | 34, 19 | recid2d 11604 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · ((coeff‘𝑎)‘(deg‘𝑎))) = 1) |
79 | 61, 77, 78 | 3eqtrd 2781 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎))‘(degAA‘𝐴)) = 1) |
80 | | fveqeq2 6726 |
. . . . . 6
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) → ((deg‘𝑝) =
(degAA‘𝐴)
↔ (deg‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)) =
(degAA‘𝐴))) |
81 | | fveq1 6716 |
. . . . . . 7
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) → (𝑝‘𝐴) = (((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)‘𝐴)) |
82 | 81 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) → ((𝑝‘𝐴) = 0 ↔ (((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)‘𝐴) = 0)) |
83 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) → (coeff‘𝑝) = (coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎))) |
84 | 83 | fveq1d 6719 |
. . . . . . 7
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) → ((coeff‘𝑝)‘(degAA‘𝐴)) = ((coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎))‘(degAA‘𝐴))) |
85 | 84 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) → (((coeff‘𝑝)‘(degAA‘𝐴)) = 1 ↔
((coeff‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎))‘(degAA‘𝐴)) = 1)) |
86 | 80, 82, 85 | 3anbi123d 1438 |
. . . . 5
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) → (((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ↔
((deg‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)) =
(degAA‘𝐴)
∧ (((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)‘𝐴) = 0 ∧ ((coeff‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎))‘(degAA‘𝐴)) = 1))) |
87 | 86 | rspcev 3537 |
. . . 4
⊢
((((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎) ∈ (Poly‘ℚ)
∧ ((deg‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)) =
(degAA‘𝐴)
∧ (((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎)‘𝐴) = 0 ∧ ((coeff‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘f · 𝑎))‘(degAA‘𝐴)) = 1)) → ∃𝑝 ∈
(Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) |
88 | 31, 40, 58, 79, 87 | syl13anc 1374 |
. . 3
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ∃𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) |
89 | | dgraalem 40673 |
. . . 4
⊢ (𝐴 ∈ 𝔸 →
((degAA‘𝐴)
∈ ℕ ∧ ∃𝑎 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0))) |
90 | 89 | simprd 499 |
. . 3
⊢ (𝐴 ∈ 𝔸 →
∃𝑎 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0)) |
91 | 88, 90 | r19.29a 3208 |
. 2
⊢ (𝐴 ∈ 𝔸 →
∃𝑝 ∈
(Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) |
92 | | simp2 1139 |
. . . . . . . . . . 11
⊢
(((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) → (𝑝‘𝐴) = 0) |
93 | | simp2 1139 |
. . . . . . . . . . 11
⊢
(((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1) → (𝑎‘𝐴) = 0) |
94 | 92, 93 | anim12i 616 |
. . . . . . . . . 10
⊢
((((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) → ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) |
95 | | plyf 25092 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ (Poly‘ℚ)
→ 𝑝:ℂ⟶ℂ) |
96 | 95 | ffnd 6546 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ (Poly‘ℚ)
→ 𝑝 Fn
ℂ) |
97 | 96 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) → 𝑝 Fn ℂ) |
98 | 46 | ffnd 6546 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (Poly‘ℚ)
→ 𝑎 Fn
ℂ) |
99 | 98 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) → 𝑎 Fn ℂ) |
100 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) → ℂ ∈
V) |
101 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → (𝑝‘𝐴) = 0) |
102 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → (𝑎‘𝐴) = 0) |
103 | 97, 99, 100, 100, 51, 101, 102 | ofval 7479 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → ((𝑝 ∘f − 𝑎)‘𝐴) = (0 − 0)) |
104 | 41, 103 | sylan2 596 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ 𝔸) → ((𝑝 ∘f −
𝑎)‘𝐴) = (0 − 0)) |
105 | | 0m0e0 11950 |
. . . . . . . . . . . 12
⊢ (0
− 0) = 0 |
106 | 104, 105 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ 𝔸) → ((𝑝 ∘f −
𝑎)‘𝐴) = 0) |
107 | 106 | ex 416 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) → (𝐴 ∈ 𝔸 → ((𝑝 ∘f −
𝑎)‘𝐴) = 0)) |
108 | 94, 107 | sylan2 596 |
. . . . . . . . 9
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (𝐴 ∈ 𝔸 → ((𝑝 ∘f −
𝑎)‘𝐴) = 0)) |
109 | 108 | com12 32 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝔸 →
(((𝑝 ∈
(Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ)) ∧
(((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → ((𝑝 ∘f −
𝑎)‘𝐴) = 0)) |
110 | 109 | impl 459 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → ((𝑝 ∘f −
𝑎)‘𝐴) = 0) |
111 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → 𝐴 ∈
𝔸) |
112 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → 𝑝 ∈
(Poly‘ℚ)) |
113 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → 𝑎 ∈
(Poly‘ℚ)) |
114 | 26 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → (𝑏 + 𝑐) ∈ ℚ) |
115 | 28 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → (𝑏 · 𝑐) ∈ ℚ) |
116 | | 1z 12207 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
117 | | zq 12550 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
118 | | qnegcl 12562 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℚ → -1 ∈ ℚ) |
119 | 116, 117,
118 | mp2b 10 |
. . . . . . . . . . 11
⊢ -1 ∈
ℚ |
120 | 119 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → -1 ∈ ℚ) |
121 | 112, 113,
114, 115, 120 | plysub 25113 |
. . . . . . . . 9
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → (𝑝 ∘f − 𝑎) ∈
(Poly‘ℚ)) |
122 | 121 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (𝑝 ∘f −
𝑎) ∈
(Poly‘ℚ)) |
123 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → 𝑝 ∈
(Poly‘ℚ)) |
124 | | simplrr 778 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → 𝑎 ∈
(Poly‘ℚ)) |
125 | | simprr1 1223 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘𝑎) =
(degAA‘𝐴)) |
126 | | simprl1 1220 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘𝑝) =
(degAA‘𝐴)) |
127 | 125, 126 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘𝑎) =
(deg‘𝑝)) |
128 | 62 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(degAA‘𝐴)
∈ ℕ) |
129 | 126, 128 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘𝑝) ∈
ℕ) |
130 | | simprl3 1222 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑝)‘(degAA‘𝐴)) = 1) |
131 | 126 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑝)‘(deg‘𝑝)) = ((coeff‘𝑝)‘(degAA‘𝐴))) |
132 | 126 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑎)‘(deg‘𝑝)) = ((coeff‘𝑎)‘(degAA‘𝐴))) |
133 | | simprr3 1225 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑎)‘(degAA‘𝐴)) = 1) |
134 | 132, 133 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑎)‘(deg‘𝑝)) = 1) |
135 | 130, 131,
134 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑝)‘(deg‘𝑝)) = ((coeff‘𝑎)‘(deg‘𝑝))) |
136 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(deg‘𝑝) =
(deg‘𝑝) |
137 | 136 | dgrsub2 40663 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((deg‘𝑎) = (deg‘𝑝) ∧ (deg‘𝑝) ∈ ℕ ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = ((coeff‘𝑎)‘(deg‘𝑝)))) → (deg‘(𝑝 ∘f −
𝑎)) < (deg‘𝑝)) |
138 | 123, 124,
127, 129, 135, 137 | syl23anc 1379 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘(𝑝
∘f − 𝑎)) < (deg‘𝑝)) |
139 | 138, 126 | breqtrd 5079 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘(𝑝
∘f − 𝑎)) < (degAA‘𝐴)) |
140 | | dgraa0p 40677 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝔸 ∧ (𝑝 ∘f −
𝑎) ∈
(Poly‘ℚ) ∧ (deg‘(𝑝 ∘f − 𝑎)) <
(degAA‘𝐴))
→ (((𝑝
∘f − 𝑎)‘𝐴) = 0 ↔ (𝑝 ∘f − 𝑎) =
0𝑝)) |
141 | 111, 122,
139, 140 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (((𝑝 ∘f −
𝑎)‘𝐴) = 0 ↔ (𝑝 ∘f − 𝑎) =
0𝑝)) |
142 | 110, 141 | mpbid 235 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (𝑝 ∘f −
𝑎) =
0𝑝) |
143 | | df-0p 24567 |
. . . . . 6
⊢
0𝑝 = (ℂ × {0}) |
144 | 142, 143 | eqtrdi 2794 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (𝑝 ∘f −
𝑎) = (ℂ ×
{0})) |
145 | | ofsubeq0 11827 |
. . . . . . . 8
⊢ ((ℂ
∈ V ∧ 𝑝:ℂ⟶ℂ ∧ 𝑎:ℂ⟶ℂ) →
((𝑝 ∘f
− 𝑎) = (ℂ
× {0}) ↔ 𝑝 =
𝑎)) |
146 | 49, 145 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑝:ℂ⟶ℂ ∧
𝑎:ℂ⟶ℂ)
→ ((𝑝
∘f − 𝑎) = (ℂ × {0}) ↔ 𝑝 = 𝑎)) |
147 | 95, 46, 146 | syl2an 599 |
. . . . . 6
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → ((𝑝 ∘f − 𝑎) = (ℂ × {0}) ↔
𝑝 = 𝑎)) |
148 | 147 | ad2antlr 727 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → ((𝑝 ∘f −
𝑎) = (ℂ × {0})
↔ 𝑝 = 𝑎)) |
149 | 144, 148 | mpbid 235 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → 𝑝 = 𝑎) |
150 | 149 | ex 416 |
. . 3
⊢ ((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) → ((((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) → 𝑝 = 𝑎)) |
151 | 150 | ralrimivva 3112 |
. 2
⊢ (𝐴 ∈ 𝔸 →
∀𝑝 ∈
(Poly‘ℚ)∀𝑎 ∈
(Poly‘ℚ)((((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) → 𝑝 = 𝑎)) |
152 | | fveqeq2 6726 |
. . . 4
⊢ (𝑝 = 𝑎 → ((deg‘𝑝) = (degAA‘𝐴) ↔ (deg‘𝑎) = (degAA‘𝐴))) |
153 | | fveq1 6716 |
. . . . 5
⊢ (𝑝 = 𝑎 → (𝑝‘𝐴) = (𝑎‘𝐴)) |
154 | 153 | eqeq1d 2739 |
. . . 4
⊢ (𝑝 = 𝑎 → ((𝑝‘𝐴) = 0 ↔ (𝑎‘𝐴) = 0)) |
155 | | fveq2 6717 |
. . . . . 6
⊢ (𝑝 = 𝑎 → (coeff‘𝑝) = (coeff‘𝑎)) |
156 | 155 | fveq1d 6719 |
. . . . 5
⊢ (𝑝 = 𝑎 → ((coeff‘𝑝)‘(degAA‘𝐴)) = ((coeff‘𝑎)‘(degAA‘𝐴))) |
157 | 156 | eqeq1d 2739 |
. . . 4
⊢ (𝑝 = 𝑎 → (((coeff‘𝑝)‘(degAA‘𝐴)) = 1 ↔
((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) |
158 | 152, 154,
157 | 3anbi123d 1438 |
. . 3
⊢ (𝑝 = 𝑎 → (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ↔ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) |
159 | 158 | reu4 3644 |
. 2
⊢
(∃!𝑝 ∈
(Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ↔ (∃𝑝 ∈
(Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ∀𝑝 ∈
(Poly‘ℚ)∀𝑎 ∈
(Poly‘ℚ)((((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) → 𝑝 = 𝑎))) |
160 | 91, 151, 159 | sylanbrc 586 |
1
⊢ (𝐴 ∈ 𝔸 →
∃!𝑝 ∈
(Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) |