Step | Hyp | Ref
| Expression |
1 | | rabid 3430 |
. . 3
β’ (π β {π β β β£ βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)} β (π β β β§ βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1))) |
2 | | qsscn 12892 |
. . . . 5
β’ β
β β |
3 | | itgoval 41517 |
. . . . 5
β’ (β
β β β (IntgOverββ) = {π β β β£ βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) |
4 | 2, 3 | ax-mp 5 |
. . . 4
β’
(IntgOverββ) = {π β β β£ βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)} |
5 | 4 | eleq2i 2830 |
. . 3
β’ (π β (IntgOverββ)
β π β {π β β β£
βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) |
6 | | aacn 25693 |
. . . . 5
β’ (π β πΈ β π β
β) |
7 | | mpaacl 41509 |
. . . . . 6
β’ (π β πΈ β
(minPolyAAβπ) β
(Polyββ)) |
8 | | mpaaroot 41511 |
. . . . . 6
β’ (π β πΈ β
((minPolyAAβπ)βπ) = 0) |
9 | | mpaadgr 41510 |
. . . . . . . 8
β’ (π β πΈ β
(degβ(minPolyAAβπ)) = (degAAβπ)) |
10 | 9 | fveq2d 6851 |
. . . . . . 7
β’ (π β πΈ β
((coeffβ(minPolyAAβπ))β(degβ(minPolyAAβπ))) =
((coeffβ(minPolyAAβπ))β(degAAβπ))) |
11 | | mpaamn 41512 |
. . . . . . 7
β’ (π β πΈ β
((coeffβ(minPolyAAβπ))β(degAAβπ)) = 1) |
12 | 10, 11 | eqtrd 2777 |
. . . . . 6
β’ (π β πΈ β
((coeffβ(minPolyAAβπ))β(degβ(minPolyAAβπ))) = 1) |
13 | | fveq1 6846 |
. . . . . . . . 9
β’ (π = (minPolyAAβπ) β (πβπ) = ((minPolyAAβπ)βπ)) |
14 | 13 | eqeq1d 2739 |
. . . . . . . 8
β’ (π = (minPolyAAβπ) β ((πβπ) = 0 β ((minPolyAAβπ)βπ) = 0)) |
15 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = (minPolyAAβπ) β (coeffβπ) =
(coeffβ(minPolyAAβπ))) |
16 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = (minPolyAAβπ) β (degβπ) =
(degβ(minPolyAAβπ))) |
17 | 15, 16 | fveq12d 6854 |
. . . . . . . . 9
β’ (π = (minPolyAAβπ) β ((coeffβπ)β(degβπ)) =
((coeffβ(minPolyAAβπ))β(degβ(minPolyAAβπ)))) |
18 | 17 | eqeq1d 2739 |
. . . . . . . 8
β’ (π = (minPolyAAβπ) β (((coeffβπ)β(degβπ)) = 1 β
((coeffβ(minPolyAAβπ))β(degβ(minPolyAAβπ))) = 1)) |
19 | 14, 18 | anbi12d 632 |
. . . . . . 7
β’ (π = (minPolyAAβπ) β (((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1) β (((minPolyAAβπ)βπ) = 0 β§
((coeffβ(minPolyAAβπ))β(degβ(minPolyAAβπ))) = 1))) |
20 | 19 | rspcev 3584 |
. . . . . 6
β’
(((minPolyAAβπ) β (Polyββ) β§
(((minPolyAAβπ)βπ) = 0 β§
((coeffβ(minPolyAAβπ))β(degβ(minPolyAAβπ))) = 1)) β βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) |
21 | 7, 8, 12, 20 | syl12anc 836 |
. . . . 5
β’ (π β πΈ β
βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) |
22 | 6, 21 | jca 513 |
. . . 4
β’ (π β πΈ β (π β β β§
βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1))) |
23 | | simpl 484 |
. . . . . . . . 9
β’ ((π β (Polyββ)
β§ ((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) β π β
(Polyββ)) |
24 | | coe0 25633 |
. . . . . . . . . . . . . . 15
β’
(coeffβ0π) = (β0 Γ
{0}) |
25 | 24 | fveq1i 6848 |
. . . . . . . . . . . . . 14
β’
((coeffβ0π)β(degβ0π))
= ((β0 Γ
{0})β(degβ0π)) |
26 | | dgr0 25639 |
. . . . . . . . . . . . . . . 16
β’
(degβ0π) = 0 |
27 | | 0nn0 12435 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β0 |
28 | 26, 27 | eqeltri 2834 |
. . . . . . . . . . . . . . 15
β’
(degβ0π) β
β0 |
29 | | c0ex 11156 |
. . . . . . . . . . . . . . . 16
β’ 0 β
V |
30 | 29 | fvconst2 7158 |
. . . . . . . . . . . . . . 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 2765 |
. . . . . . . . . . . . 13
β’
((coeffβ0π)β(degβ0π))
= 0 |
33 | | 0ne1 12231 |
. . . . . . . . . . . . 13
β’ 0 β
1 |
34 | 32, 33 | eqnetri 3015 |
. . . . . . . . . . . 12
β’
((coeffβ0π)β(degβ0π))
β 1 |
35 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = 0π β
(coeffβπ) =
(coeffβ0π)) |
36 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = 0π β
(degβπ) =
(degβ0π)) |
37 | 35, 36 | fveq12d 6854 |
. . . . . . . . . . . . 13
β’ (π = 0π β
((coeffβπ)β(degβπ)) =
((coeffβ0π)β(degβ0π))) |
38 | 37 | neeq1d 3004 |
. . . . . . . . . . . 12
β’ (π = 0π β
(((coeffβπ)β(degβπ)) β 1 β
((coeffβ0π)β(degβ0π))
β 1)) |
39 | 34, 38 | mpbiri 258 |
. . . . . . . . . . 11
β’ (π = 0π β
((coeffβπ)β(degβπ)) β 1) |
40 | 39 | necon2i 2979 |
. . . . . . . . . 10
β’
(((coeffβπ)β(degβπ)) = 1 β π β 0π) |
41 | 40 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β (Polyββ)
β§ ((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) β π β
0π) |
42 | | eldifsn 4752 |
. . . . . . . . 9
β’ (π β ((Polyββ)
β {0π}) β (π β (Polyββ) β§ π β
0π)) |
43 | 23, 41, 42 | sylanbrc 584 |
. . . . . . . 8
β’ ((π β (Polyββ)
β§ ((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) β π β ((Polyββ)
β {0π})) |
44 | | simprl 770 |
. . . . . . . 8
β’ ((π β (Polyββ)
β§ ((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) β (πβπ) = 0) |
45 | 43, 44 | jca 513 |
. . . . . . 7
β’ ((π β (Polyββ)
β§ ((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) β (π β ((Polyββ)
β {0π}) β§ (πβπ) = 0)) |
46 | 45 | reximi2 3083 |
. . . . . 6
β’
(βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1) β βπ β ((Polyββ) β
{0π})(πβπ) = 0) |
47 | 46 | anim2i 618 |
. . . . 5
β’ ((π β β β§
βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) β (π β β β§ βπ β ((Polyββ)
β {0π})(πβπ) = 0)) |
48 | | elqaa 25698 |
. . . . 5
β’ (π β πΈ β (π β β β§
βπ β
((Polyββ) β {0π})(πβπ) = 0)) |
49 | 47, 48 | sylibr 233 |
. . . 4
β’ ((π β β β§
βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1)) β π β πΈ) |
50 | 22, 49 | impbii 208 |
. . 3
β’ (π β πΈ β (π β β β§
βπ β
(Polyββ)((πβπ) = 0 β§ ((coeffβπ)β(degβπ)) = 1))) |
51 | 1, 5, 50 | 3bitr4ri 304 |
. 2
β’ (π β πΈ β π β
(IntgOverββ)) |
52 | 51 | eqriv 2734 |
1
β’ πΈ
= (IntgOverββ) |