Step | Hyp | Ref
| Expression |
1 | | cmpaa 41511 |
. 2
class
minPolyAA |
2 | | vx |
. . 3
setvar π₯ |
3 | | caa 25690 |
. . 3
class
πΈ |
4 | | vp |
. . . . . . . 8
setvar π |
5 | 4 | cv 1541 |
. . . . . . 7
class π |
6 | | cdgr 25564 |
. . . . . . 7
class
deg |
7 | 5, 6 | cfv 6497 |
. . . . . 6
class
(degβπ) |
8 | 2 | cv 1541 |
. . . . . . 7
class π₯ |
9 | | cdgraa 41510 |
. . . . . . 7
class
degAA |
10 | 8, 9 | cfv 6497 |
. . . . . 6
class
(degAAβπ₯) |
11 | 7, 10 | wceq 1542 |
. . . . 5
wff
(degβπ) =
(degAAβπ₯) |
12 | 8, 5 | cfv 6497 |
. . . . . 6
class (πβπ₯) |
13 | | cc0 11056 |
. . . . . 6
class
0 |
14 | 12, 13 | wceq 1542 |
. . . . 5
wff (πβπ₯) = 0 |
15 | | ccoe 25563 |
. . . . . . . 8
class
coeff |
16 | 5, 15 | cfv 6497 |
. . . . . . 7
class
(coeffβπ) |
17 | 10, 16 | cfv 6497 |
. . . . . 6
class
((coeffβπ)β(degAAβπ₯)) |
18 | | c1 11057 |
. . . . . 6
class
1 |
19 | 17, 18 | wceq 1542 |
. . . . 5
wff
((coeffβπ)β(degAAβπ₯)) = 1 |
20 | 11, 14, 19 | w3a 1088 |
. . . 4
wff
((degβπ) =
(degAAβπ₯)
β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1) |
21 | | cq 12878 |
. . . . 5
class
β |
22 | | cply 25561 |
. . . . 5
class
Poly |
23 | 21, 22 | cfv 6497 |
. . . 4
class
(Polyββ) |
24 | 20, 4, 23 | crio 7313 |
. . 3
class
(β©π
β (Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1)) |
25 | 2, 3, 24 | cmpt 5189 |
. 2
class (π₯ β πΈ β¦
(β©π β
(Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1))) |
26 | 1, 25 | wceq 1542 |
1
wff minPolyAA =
(π₯ β πΈ β¦
(β©π β
(Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1))) |