Step | Hyp | Ref
| Expression |
1 | | rabid 3116 |
. . 3
⊢ (𝑎 ∈ {𝑎 ∈ ℂ ∣ ∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)} ↔ (𝑎 ∈ ℂ ∧ ∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1))) |
2 | | qsscn 11799 |
. . . . 5
⊢ ℚ
⊆ ℂ |
3 | | itgoval 37731 |
. . . . 5
⊢ (ℚ
⊆ ℂ → (IntgOver‘ℚ) = {𝑎 ∈ ℂ ∣ ∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)}) |
4 | 2, 3 | ax-mp 5 |
. . . 4
⊢
(IntgOver‘ℚ) = {𝑎 ∈ ℂ ∣ ∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)} |
5 | 4 | eleq2i 2693 |
. . 3
⊢ (𝑎 ∈ (IntgOver‘ℚ)
↔ 𝑎 ∈ {𝑎 ∈ ℂ ∣
∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)}) |
6 | | aacn 24072 |
. . . . 5
⊢ (𝑎 ∈ 𝔸 → 𝑎 ∈
ℂ) |
7 | | mpaacl 37723 |
. . . . . 6
⊢ (𝑎 ∈ 𝔸 →
(minPolyAA‘𝑎) ∈
(Poly‘ℚ)) |
8 | | mpaaroot 37725 |
. . . . . 6
⊢ (𝑎 ∈ 𝔸 →
((minPolyAA‘𝑎)‘𝑎) = 0) |
9 | | mpaadgr 37724 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝔸 →
(deg‘(minPolyAA‘𝑎)) = (degAA‘𝑎)) |
10 | 9 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑎 ∈ 𝔸 →
((coeff‘(minPolyAA‘𝑎))‘(deg‘(minPolyAA‘𝑎))) =
((coeff‘(minPolyAA‘𝑎))‘(degAA‘𝑎))) |
11 | | mpaamn 37726 |
. . . . . . 7
⊢ (𝑎 ∈ 𝔸 →
((coeff‘(minPolyAA‘𝑎))‘(degAA‘𝑎)) = 1) |
12 | 10, 11 | eqtrd 2656 |
. . . . . 6
⊢ (𝑎 ∈ 𝔸 →
((coeff‘(minPolyAA‘𝑎))‘(deg‘(minPolyAA‘𝑎))) = 1) |
13 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑏 = (minPolyAA‘𝑎) → (𝑏‘𝑎) = ((minPolyAA‘𝑎)‘𝑎)) |
14 | 13 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑏 = (minPolyAA‘𝑎) → ((𝑏‘𝑎) = 0 ↔ ((minPolyAA‘𝑎)‘𝑎) = 0)) |
15 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑏 = (minPolyAA‘𝑎) → (coeff‘𝑏) =
(coeff‘(minPolyAA‘𝑎))) |
16 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑏 = (minPolyAA‘𝑎) → (deg‘𝑏) =
(deg‘(minPolyAA‘𝑎))) |
17 | 15, 16 | fveq12d 6197 |
. . . . . . . . 9
⊢ (𝑏 = (minPolyAA‘𝑎) → ((coeff‘𝑏)‘(deg‘𝑏)) =
((coeff‘(minPolyAA‘𝑎))‘(deg‘(minPolyAA‘𝑎)))) |
18 | 17 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑏 = (minPolyAA‘𝑎) → (((coeff‘𝑏)‘(deg‘𝑏)) = 1 ↔
((coeff‘(minPolyAA‘𝑎))‘(deg‘(minPolyAA‘𝑎))) = 1)) |
19 | 14, 18 | anbi12d 747 |
. . . . . . 7
⊢ (𝑏 = (minPolyAA‘𝑎) → (((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1) ↔ (((minPolyAA‘𝑎)‘𝑎) = 0 ∧
((coeff‘(minPolyAA‘𝑎))‘(deg‘(minPolyAA‘𝑎))) = 1))) |
20 | 19 | rspcev 3309 |
. . . . . 6
⊢
(((minPolyAA‘𝑎) ∈ (Poly‘ℚ) ∧
(((minPolyAA‘𝑎)‘𝑎) = 0 ∧
((coeff‘(minPolyAA‘𝑎))‘(deg‘(minPolyAA‘𝑎))) = 1)) → ∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) |
21 | 7, 8, 12, 20 | syl12anc 1324 |
. . . . 5
⊢ (𝑎 ∈ 𝔸 →
∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) |
22 | 6, 21 | jca 554 |
. . . 4
⊢ (𝑎 ∈ 𝔸 → (𝑎 ∈ ℂ ∧
∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1))) |
23 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑏 ∈ (Poly‘ℚ)
∧ ((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) → 𝑏 ∈
(Poly‘ℚ)) |
24 | | coe0 24012 |
. . . . . . . . . . . . . . 15
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
25 | 24 | fveq1i 6192 |
. . . . . . . . . . . . . 14
⊢
((coeff‘0𝑝)‘(deg‘0𝑝))
= ((ℕ0 ×
{0})‘(deg‘0𝑝)) |
26 | | dgr0 24018 |
. . . . . . . . . . . . . . . 16
⊢
(deg‘0𝑝) = 0 |
27 | | 0nn0 11307 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℕ0 |
28 | 26, 27 | eqeltri 2697 |
. . . . . . . . . . . . . . 15
⊢
(deg‘0𝑝) ∈
ℕ0 |
29 | | c0ex 10034 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
V |
30 | 29 | fvconst2 6469 |
. . . . . . . . . . . . . . 15
⊢
((deg‘0𝑝) ∈ ℕ0 →
((ℕ0 × {0})‘(deg‘0𝑝)) =
0) |
31 | 28, 30 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((ℕ0 ×
{0})‘(deg‘0𝑝)) = 0 |
32 | 25, 31 | eqtri 2644 |
. . . . . . . . . . . . 13
⊢
((coeff‘0𝑝)‘(deg‘0𝑝))
= 0 |
33 | | 0ne1 11088 |
. . . . . . . . . . . . 13
⊢ 0 ≠
1 |
34 | 32, 33 | eqnetri 2864 |
. . . . . . . . . . . 12
⊢
((coeff‘0𝑝)‘(deg‘0𝑝))
≠ 1 |
35 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 0𝑝 →
(coeff‘𝑏) =
(coeff‘0𝑝)) |
36 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 0𝑝 →
(deg‘𝑏) =
(deg‘0𝑝)) |
37 | 35, 36 | fveq12d 6197 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 0𝑝 →
((coeff‘𝑏)‘(deg‘𝑏)) =
((coeff‘0𝑝)‘(deg‘0𝑝))) |
38 | 37 | neeq1d 2853 |
. . . . . . . . . . . 12
⊢ (𝑏 = 0𝑝 →
(((coeff‘𝑏)‘(deg‘𝑏)) ≠ 1 ↔
((coeff‘0𝑝)‘(deg‘0𝑝))
≠ 1)) |
39 | 34, 38 | mpbiri 248 |
. . . . . . . . . . 11
⊢ (𝑏 = 0𝑝 →
((coeff‘𝑏)‘(deg‘𝑏)) ≠ 1) |
40 | 39 | necon2i 2828 |
. . . . . . . . . 10
⊢
(((coeff‘𝑏)‘(deg‘𝑏)) = 1 → 𝑏 ≠ 0𝑝) |
41 | 40 | ad2antll 765 |
. . . . . . . . 9
⊢ ((𝑏 ∈ (Poly‘ℚ)
∧ ((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) → 𝑏 ≠
0𝑝) |
42 | | eldifsn 4317 |
. . . . . . . . 9
⊢ (𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ↔ (𝑏 ∈ (Poly‘ℚ) ∧ 𝑏 ≠
0𝑝)) |
43 | 23, 41, 42 | sylanbrc 698 |
. . . . . . . 8
⊢ ((𝑏 ∈ (Poly‘ℚ)
∧ ((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) → 𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})) |
44 | | simprl 794 |
. . . . . . . 8
⊢ ((𝑏 ∈ (Poly‘ℚ)
∧ ((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) → (𝑏‘𝑎) = 0) |
45 | 43, 44 | jca 554 |
. . . . . . 7
⊢ ((𝑏 ∈ (Poly‘ℚ)
∧ ((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) → (𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ∧ (𝑏‘𝑎) = 0)) |
46 | 45 | reximi2 3010 |
. . . . . 6
⊢
(∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1) → ∃𝑏 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑏‘𝑎) = 0) |
47 | 46 | anim2i 593 |
. . . . 5
⊢ ((𝑎 ∈ ℂ ∧
∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) → (𝑎 ∈ ℂ ∧ ∃𝑏 ∈ ((Poly‘ℚ)
∖ {0𝑝})(𝑏‘𝑎) = 0)) |
48 | | elqaa 24077 |
. . . . 5
⊢ (𝑎 ∈ 𝔸 ↔ (𝑎 ∈ ℂ ∧
∃𝑏 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑏‘𝑎) = 0)) |
49 | 47, 48 | sylibr 224 |
. . . 4
⊢ ((𝑎 ∈ ℂ ∧
∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1)) → 𝑎 ∈ 𝔸) |
50 | 22, 49 | impbii 199 |
. . 3
⊢ (𝑎 ∈ 𝔸 ↔ (𝑎 ∈ ℂ ∧
∃𝑏 ∈
(Poly‘ℚ)((𝑏‘𝑎) = 0 ∧ ((coeff‘𝑏)‘(deg‘𝑏)) = 1))) |
51 | 1, 5, 50 | 3bitr4ri 293 |
. 2
⊢ (𝑎 ∈ 𝔸 ↔ 𝑎 ∈
(IntgOver‘ℚ)) |
52 | 51 | eqriv 2619 |
1
⊢ 𝔸
= (IntgOver‘ℚ) |