Step | Hyp | Ref
| Expression |
1 | | qsscn 11799 |
. . . . . 6
⊢ ℚ
⊆ ℂ |
2 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝}) → 𝑎 ∈
(Poly‘ℚ)) |
3 | 2 | ad2antlr 763 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → 𝑎 ∈
(Poly‘ℚ)) |
4 | | zssq 11795 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℚ |
5 | | 0z 11388 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
6 | 4, 5 | sselii 3600 |
. . . . . . . . 9
⊢ 0 ∈
ℚ |
7 | | eqid 2622 |
. . . . . . . . . 10
⊢
(coeff‘𝑎) =
(coeff‘𝑎) |
8 | 7 | coef2 23987 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (Poly‘ℚ)
∧ 0 ∈ ℚ) → (coeff‘𝑎):ℕ0⟶ℚ) |
9 | 3, 6, 8 | sylancl 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (coeff‘𝑎):ℕ0⟶ℚ) |
10 | | dgrcl 23989 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Poly‘ℚ)
→ (deg‘𝑎) ∈
ℕ0) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (deg‘𝑎) ∈
ℕ0) |
12 | 9, 11 | ffvelrnd 6360 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘𝑎)‘(deg‘𝑎)) ∈
ℚ) |
13 | | eldifsni 4320 |
. . . . . . . . 9
⊢ (𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝}) → 𝑎 ≠ 0𝑝) |
14 | 13 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → 𝑎 ≠ 0𝑝) |
15 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(deg‘𝑎) =
(deg‘𝑎) |
16 | 15, 7 | dgreq0 24021 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (Poly‘ℚ)
→ (𝑎 =
0𝑝 ↔ ((coeff‘𝑎)‘(deg‘𝑎)) = 0)) |
17 | 16 | necon3bid 2838 |
. . . . . . . . 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 222 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘𝑎)‘(deg‘𝑎)) ≠ 0) |
20 | | qreccl 11808 |
. . . . . . 7
⊢
((((coeff‘𝑎)‘(deg‘𝑎)) ∈ ℚ ∧ ((coeff‘𝑎)‘(deg‘𝑎)) ≠ 0) → (1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ ℚ) |
21 | 12, 19, 20 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (1 / ((coeff‘𝑎)‘(deg‘𝑎))) ∈
ℚ) |
22 | | plyconst 23962 |
. . . . . 6
⊢ ((ℚ
⊆ ℂ ∧ (1 / ((coeff‘𝑎)‘(deg‘𝑎))) ∈ ℚ) → (ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈
(Poly‘ℚ)) |
23 | 1, 21, 22 | sylancr 695 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∈
(Poly‘ℚ)) |
24 | | simpl 473 |
. . . . . 6
⊢
(((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
→ (ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈
(Poly‘ℚ)) |
25 | | simpr 477 |
. . . . . 6
⊢
(((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
→ 𝑎 ∈
(Poly‘ℚ)) |
26 | | qaddcl 11804 |
. . . . . . 7
⊢ ((𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ) → (𝑏 + 𝑐) ∈ ℚ) |
27 | 26 | adantl 482 |
. . . . . 6
⊢
((((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
∧ (𝑏 ∈ ℚ
∧ 𝑐 ∈ ℚ))
→ (𝑏 + 𝑐) ∈
ℚ) |
28 | | qmulcl 11806 |
. . . . . . 7
⊢ ((𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ) → (𝑏 · 𝑐) ∈ ℚ) |
29 | 28 | adantl 482 |
. . . . . 6
⊢
((((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
∧ (𝑏 ∈ ℚ
∧ 𝑐 ∈ ℚ))
→ (𝑏 · 𝑐) ∈
ℚ) |
30 | 24, 25, 27, 29 | plymul 23974 |
. . . . 5
⊢
(((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∈ (Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ))
→ ((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) ∈
(Poly‘ℚ)) |
31 | 23, 3, 30 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) ∈
(Poly‘ℚ)) |
32 | 7 | coef3 23988 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Poly‘ℚ)
→ (coeff‘𝑎):ℕ0⟶ℂ) |
33 | 3, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (coeff‘𝑎):ℕ0⟶ℂ) |
34 | 33, 11 | ffvelrnd 6360 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘𝑎)‘(deg‘𝑎)) ∈
ℂ) |
35 | 34, 19 | reccld 10794 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (1 / ((coeff‘𝑎)‘(deg‘𝑎))) ∈
ℂ) |
36 | 34, 19 | recne0d 10795 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (1 / ((coeff‘𝑎)‘(deg‘𝑎))) ≠ 0) |
37 | | dgrmulc 24027 |
. . . . . 6
⊢ (((1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ ℂ ∧ (1 /
((coeff‘𝑎)‘(deg‘𝑎))) ≠ 0 ∧ 𝑎 ∈ (Poly‘ℚ)) →
(deg‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)) = (deg‘𝑎)) |
38 | 35, 36, 3, 37 | syl3anc 1326 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (deg‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)) = (deg‘𝑎)) |
39 | | simprl 794 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (deg‘𝑎) = (degAA‘𝐴)) |
40 | 38, 39 | eqtrd 2656 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (deg‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)) =
(degAA‘𝐴)) |
41 | | aacn 24072 |
. . . . . . 7
⊢ (𝐴 ∈ 𝔸 → 𝐴 ∈
ℂ) |
42 | 41 | ad2antrr 762 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → 𝐴 ∈ ℂ) |
43 | | ovex 6678 |
. . . . . . . 8
⊢ (1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ V |
44 | | fnconstg 6093 |
. . . . . . . 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 23954 |
. . . . . . . 8
⊢ (𝑎 ∈ (Poly‘ℚ)
→ 𝑎:ℂ⟶ℂ) |
47 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑎:ℂ⟶ℂ →
𝑎 Fn
ℂ) |
48 | 3, 46, 47 | 3syl 18 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → 𝑎 Fn ℂ) |
49 | | cnex 10017 |
. . . . . . . 8
⊢ ℂ
∈ V |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ℂ ∈
V) |
51 | | inidm 3822 |
. . . . . . 7
⊢ (ℂ
∩ ℂ) = ℂ |
52 | 43 | fvconst2 6469 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))})‘𝐴) = (1 / ((coeff‘𝑎)‘(deg‘𝑎)))) |
53 | 52 | adantl 482 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → ((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))})‘𝐴) = (1 / ((coeff‘𝑎)‘(deg‘𝑎)))) |
54 | | simplrr 801 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → (𝑎‘𝐴) = 0) |
55 | 45, 48, 50, 50, 51, 53, 54 | ofval 6906 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → (((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)‘𝐴) = ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · 0)) |
56 | 42, 55 | mpdan 702 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)‘𝐴) = ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · 0)) |
57 | 35 | mul01d 10235 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · 0) =
0) |
58 | 56, 57 | eqtrd 2656 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)‘𝐴) = 0) |
59 | | coemulc 24011 |
. . . . . . 7
⊢ (((1 /
((coeff‘𝑎)‘(deg‘𝑎))) ∈ ℂ ∧ 𝑎 ∈ (Poly‘ℚ)) →
(coeff‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)) = ((ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
(coeff‘𝑎))) |
60 | 35, 3, 59 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)) = ((ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
(coeff‘𝑎))) |
61 | 60 | fveq1d 6193 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎))‘(degAA‘𝐴)) = (((ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
(coeff‘𝑎))‘(degAA‘𝐴))) |
62 | | dgraacl 37716 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝔸 →
(degAA‘𝐴)
∈ ℕ) |
63 | 62 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (degAA‘𝐴) ∈
ℕ) |
64 | 63 | nnnn0d 11351 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (degAA‘𝐴) ∈
ℕ0) |
65 | | fnconstg 6093 |
. . . . . . . 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 | | ffn 6045 |
. . . . . . . 8
⊢
((coeff‘𝑎):ℕ0⟶ℂ →
(coeff‘𝑎) Fn
ℕ0) |
68 | 33, 67 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (coeff‘𝑎) Fn
ℕ0) |
69 | | nn0ex 11298 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
70 | 69 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ℕ0 ∈
V) |
71 | | inidm 3822 |
. . . . . . 7
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
72 | 43 | fvconst2 6469 |
. . . . . . . 8
⊢
((degAA‘𝐴) ∈ ℕ0 →
((ℕ0 × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))})‘(degAA‘𝐴)) = (1 / ((coeff‘𝑎)‘(deg‘𝑎)))) |
73 | 72 | adantl 482 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ ((ℕ0 × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))})‘(degAA‘𝐴)) = (1 / ((coeff‘𝑎)‘(deg‘𝑎)))) |
74 | | simplrl 800 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ (deg‘𝑎) =
(degAA‘𝐴)) |
75 | 74 | eqcomd 2628 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ (degAA‘𝐴) = (deg‘𝑎)) |
76 | 75 | fveq2d 6195 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ ((coeff‘𝑎)‘(degAA‘𝐴)) = ((coeff‘𝑎)‘(deg‘𝑎))) |
77 | 66, 68, 70, 70, 71, 73, 76 | ofval 6906 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) ∧ (degAA‘𝐴) ∈ ℕ0)
→ (((ℕ0 × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
(coeff‘𝑎))‘(degAA‘𝐴)) = ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · ((coeff‘𝑎)‘(deg‘𝑎)))) |
78 | 64, 77 | mpdan 702 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → (((ℕ0
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
(coeff‘𝑎))‘(degAA‘𝐴)) = ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · ((coeff‘𝑎)‘(deg‘𝑎)))) |
79 | 34, 19 | recid2d 10797 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((1 / ((coeff‘𝑎)‘(deg‘𝑎))) · ((coeff‘𝑎)‘(deg‘𝑎))) = 1) |
80 | 61, 78, 79 | 3eqtrd 2660 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ((coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎))‘(degAA‘𝐴)) = 1) |
81 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) → (deg‘𝑝) = (deg‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎))) |
82 | 81 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) → ((deg‘𝑝) =
(degAA‘𝐴)
↔ (deg‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)) =
(degAA‘𝐴))) |
83 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) → (𝑝‘𝐴) = (((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)‘𝐴)) |
84 | 83 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) → ((𝑝‘𝐴) = 0 ↔ (((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)‘𝐴) = 0)) |
85 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) →
(coeff‘𝑝) =
(coeff‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎))) |
86 | 85 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) →
((coeff‘𝑝)‘(degAA‘𝐴)) = ((coeff‘((ℂ
× {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎))‘(degAA‘𝐴))) |
87 | 86 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) →
(((coeff‘𝑝)‘(degAA‘𝐴)) = 1 ↔
((coeff‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎))‘(degAA‘𝐴)) = 1)) |
88 | 82, 84, 87 | 3anbi123d 1399 |
. . . . 5
⊢ (𝑝 = ((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) →
(((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ↔
((deg‘((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)) =
(degAA‘𝐴)
∧ (((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)‘𝐴) = 0 ∧ ((coeff‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎))‘(degAA‘𝐴)) = 1))) |
89 | 88 | rspcev 3309 |
. . . 4
⊢
((((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎) ∈
(Poly‘ℚ) ∧ ((deg‘((ℂ × {(1 /
((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)) =
(degAA‘𝐴)
∧ (((ℂ × {(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎)‘𝐴) = 0 ∧ ((coeff‘((ℂ ×
{(1 / ((coeff‘𝑎)‘(deg‘𝑎)))}) ∘𝑓 ·
𝑎))‘(degAA‘𝐴)) = 1)) → ∃𝑝 ∈
(Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) |
90 | 31, 40, 58, 80, 89 | syl13anc 1328 |
. . 3
⊢ (((𝐴 ∈ 𝔸 ∧ 𝑎 ∈ ((Poly‘ℚ)
∖ {0𝑝})) ∧ ((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0)) → ∃𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) |
91 | | dgraalem 37715 |
. . . 4
⊢ (𝐴 ∈ 𝔸 →
((degAA‘𝐴)
∈ ℕ ∧ ∃𝑎 ∈ ((Poly‘ℚ) ∖
{0𝑝})((deg‘𝑎) = (degAA‘𝐴) ∧ (𝑎‘𝐴) = 0))) |
92 | 91 | simprd 479 |
. . 3
⊢ (𝐴 ∈ 𝔸 →
∃𝑎 ∈
((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0)) |
93 | 90, 92 | r19.29a 3078 |
. 2
⊢ (𝐴 ∈ 𝔸 →
∃𝑝 ∈
(Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) |
94 | | simp2 1062 |
. . . . . . . . . . 11
⊢
(((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) → (𝑝‘𝐴) = 0) |
95 | | simp2 1062 |
. . . . . . . . . . 11
⊢
(((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1) → (𝑎‘𝐴) = 0) |
96 | 94, 95 | anim12i 590 |
. . . . . . . . . 10
⊢
((((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) → ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) |
97 | | plyf 23954 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ (Poly‘ℚ)
→ 𝑝:ℂ⟶ℂ) |
98 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝:ℂ⟶ℂ →
𝑝 Fn
ℂ) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ (Poly‘ℚ)
→ 𝑝 Fn
ℂ) |
100 | 99 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) → 𝑝 Fn ℂ) |
101 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (Poly‘ℚ)
→ 𝑎 Fn
ℂ) |
102 | 101 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) → 𝑎 Fn ℂ) |
103 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) → ℂ ∈
V) |
104 | | simplrl 800 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → (𝑝‘𝐴) = 0) |
105 | | simplrr 801 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → (𝑎‘𝐴) = 0) |
106 | 100, 102,
103, 103, 51, 104, 105 | ofval 6906 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ ℂ) → ((𝑝 ∘𝑓 − 𝑎)‘𝐴) = (0 − 0)) |
107 | 41, 106 | sylan2 491 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ 𝔸) → ((𝑝 ∘𝑓
− 𝑎)‘𝐴) = (0 −
0)) |
108 | | 0m0e0 11130 |
. . . . . . . . . . . 12
⊢ (0
− 0) = 0 |
109 | 107, 108 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) ∧ 𝐴 ∈ 𝔸) → ((𝑝 ∘𝑓
− 𝑎)‘𝐴) = 0) |
110 | 109 | ex 450 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((𝑝‘𝐴) = 0 ∧ (𝑎‘𝐴) = 0)) → (𝐴 ∈ 𝔸 → ((𝑝 ∘𝑓
− 𝑎)‘𝐴) = 0)) |
111 | 96, 110 | sylan2 491 |
. . . . . . . . 9
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (𝐴 ∈ 𝔸 → ((𝑝 ∘𝑓
− 𝑎)‘𝐴) = 0)) |
112 | 111 | com12 32 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝔸 →
(((𝑝 ∈
(Poly‘ℚ) ∧ 𝑎 ∈ (Poly‘ℚ)) ∧
(((deg‘𝑝) =
(degAA‘𝐴)
∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → ((𝑝 ∘𝑓
− 𝑎)‘𝐴) = 0)) |
113 | 112 | impl 650 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → ((𝑝 ∘𝑓
− 𝑎)‘𝐴) = 0) |
114 | | simpll 790 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → 𝐴 ∈
𝔸) |
115 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → 𝑝 ∈
(Poly‘ℚ)) |
116 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → 𝑎 ∈
(Poly‘ℚ)) |
117 | 26 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → (𝑏 + 𝑐) ∈ ℚ) |
118 | 28 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → (𝑏 · 𝑐) ∈ ℚ) |
119 | | 1z 11407 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
120 | | zq 11794 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
121 | | qnegcl 11805 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℚ → -1 ∈ ℚ) |
122 | 119, 120,
121 | mp2b 10 |
. . . . . . . . . . 11
⊢ -1 ∈
ℚ |
123 | 122 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → -1 ∈ ℚ) |
124 | 115, 116,
117, 118, 123 | plysub 23975 |
. . . . . . . . 9
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → (𝑝 ∘𝑓 − 𝑎) ∈
(Poly‘ℚ)) |
125 | 124 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (𝑝 ∘𝑓
− 𝑎) ∈
(Poly‘ℚ)) |
126 | | simplrl 800 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → 𝑝 ∈
(Poly‘ℚ)) |
127 | | simplrr 801 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → 𝑎 ∈
(Poly‘ℚ)) |
128 | | simprr1 1109 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘𝑎) =
(degAA‘𝐴)) |
129 | | simprl1 1106 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘𝑝) =
(degAA‘𝐴)) |
130 | 128, 129 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘𝑎) =
(deg‘𝑝)) |
131 | 62 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(degAA‘𝐴)
∈ ℕ) |
132 | 129, 131 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘𝑝) ∈
ℕ) |
133 | | simprl3 1108 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑝)‘(degAA‘𝐴)) = 1) |
134 | 129 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑝)‘(deg‘𝑝)) = ((coeff‘𝑝)‘(degAA‘𝐴))) |
135 | 129 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑎)‘(deg‘𝑝)) = ((coeff‘𝑎)‘(degAA‘𝐴))) |
136 | | simprr3 1111 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑎)‘(degAA‘𝐴)) = 1) |
137 | 135, 136 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑎)‘(deg‘𝑝)) = 1) |
138 | 133, 134,
137 | 3eqtr4d 2666 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
((coeff‘𝑝)‘(deg‘𝑝)) = ((coeff‘𝑎)‘(deg‘𝑝))) |
139 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(deg‘𝑝) =
(deg‘𝑝) |
140 | 139 | dgrsub2 37705 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) ∧ ((deg‘𝑎) = (deg‘𝑝) ∧ (deg‘𝑝) ∈ ℕ ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = ((coeff‘𝑎)‘(deg‘𝑝)))) → (deg‘(𝑝 ∘𝑓
− 𝑎)) <
(deg‘𝑝)) |
141 | 126, 127,
130, 132, 138, 140 | syl23anc 1333 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘(𝑝
∘𝑓 − 𝑎)) < (deg‘𝑝)) |
142 | 141, 129 | breqtrd 4679 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) →
(deg‘(𝑝
∘𝑓 − 𝑎)) < (degAA‘𝐴)) |
143 | | dgraa0p 37719 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝔸 ∧ (𝑝 ∘𝑓
− 𝑎) ∈
(Poly‘ℚ) ∧ (deg‘(𝑝 ∘𝑓 − 𝑎)) <
(degAA‘𝐴))
→ (((𝑝
∘𝑓 − 𝑎)‘𝐴) = 0 ↔ (𝑝 ∘𝑓 − 𝑎) =
0𝑝)) |
144 | 114, 125,
142, 143 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (((𝑝 ∘𝑓
− 𝑎)‘𝐴) = 0 ↔ (𝑝 ∘𝑓 − 𝑎) =
0𝑝)) |
145 | 113, 144 | mpbid 222 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (𝑝 ∘𝑓
− 𝑎) =
0𝑝) |
146 | | df-0p 23437 |
. . . . . 6
⊢
0𝑝 = (ℂ × {0}) |
147 | 145, 146 | syl6eq 2672 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → (𝑝 ∘𝑓
− 𝑎) = (ℂ
× {0})) |
148 | | ofsubeq0 11017 |
. . . . . . . 8
⊢ ((ℂ
∈ V ∧ 𝑝:ℂ⟶ℂ ∧ 𝑎:ℂ⟶ℂ) →
((𝑝
∘𝑓 − 𝑎) = (ℂ × {0}) ↔ 𝑝 = 𝑎)) |
149 | 49, 148 | mp3an1 1411 |
. . . . . . 7
⊢ ((𝑝:ℂ⟶ℂ ∧
𝑎:ℂ⟶ℂ)
→ ((𝑝
∘𝑓 − 𝑎) = (ℂ × {0}) ↔ 𝑝 = 𝑎)) |
150 | 97, 46, 149 | syl2an 494 |
. . . . . 6
⊢ ((𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ)) → ((𝑝 ∘𝑓 − 𝑎) = (ℂ × {0}) ↔
𝑝 = 𝑎)) |
151 | 150 | ad2antlr 763 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → ((𝑝 ∘𝑓
− 𝑎) = (ℂ
× {0}) ↔ 𝑝 =
𝑎)) |
152 | 147, 151 | mpbid 222 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) ∧ (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) → 𝑝 = 𝑎) |
153 | 152 | ex 450 |
. . 3
⊢ ((𝐴 ∈ 𝔸 ∧ (𝑝 ∈ (Poly‘ℚ)
∧ 𝑎 ∈
(Poly‘ℚ))) → ((((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) → 𝑝 = 𝑎)) |
154 | 153 | ralrimivva 2971 |
. 2
⊢ (𝐴 ∈ 𝔸 →
∀𝑝 ∈
(Poly‘ℚ)∀𝑎 ∈
(Poly‘ℚ)((((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ∧ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) → 𝑝 = 𝑎)) |
155 | | fveq2 6191 |
. . . . 5
⊢ (𝑝 = 𝑎 → (deg‘𝑝) = (deg‘𝑎)) |
156 | 155 | eqeq1d 2624 |
. . . 4
⊢ (𝑝 = 𝑎 → ((deg‘𝑝) = (degAA‘𝐴) ↔ (deg‘𝑎) = (degAA‘𝐴))) |
157 | | fveq1 6190 |
. . . . 5
⊢ (𝑝 = 𝑎 → (𝑝‘𝐴) = (𝑎‘𝐴)) |
158 | 157 | eqeq1d 2624 |
. . . 4
⊢ (𝑝 = 𝑎 → ((𝑝‘𝐴) = 0 ↔ (𝑎‘𝐴) = 0)) |
159 | | fveq2 6191 |
. . . . . 6
⊢ (𝑝 = 𝑎 → (coeff‘𝑝) = (coeff‘𝑎)) |
160 | 159 | fveq1d 6193 |
. . . . 5
⊢ (𝑝 = 𝑎 → ((coeff‘𝑝)‘(degAA‘𝐴)) = ((coeff‘𝑎)‘(degAA‘𝐴))) |
161 | 160 | eqeq1d 2624 |
. . . 4
⊢ (𝑝 = 𝑎 → (((coeff‘𝑝)‘(degAA‘𝐴)) = 1 ↔
((coeff‘𝑎)‘(degAA‘𝐴)) = 1)) |
162 | 156, 158,
161 | 3anbi123d 1399 |
. . 3
⊢ (𝑝 = 𝑎 → (((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1) ↔ ((deg‘𝑎) =
(degAA‘𝐴)
∧ (𝑎‘𝐴) = 0 ∧ ((coeff‘𝑎)‘(degAA‘𝐴)) = 1))) |
163 | 162 | reu4 3400 |
. 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)) → 𝑝 = 𝑎))) |
164 | 93, 154, 163 | sylanbrc 698 |
1
⊢ (𝐴 ∈ 𝔸 →
∃!𝑝 ∈
(Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) |