Step | Hyp | Ref
| Expression |
1 | | cmpaa 42185 |
. 2
class
minPolyAA |
2 | | vx |
. . 3
setvar π₯ |
3 | | caa 26063 |
. . 3
class
πΈ |
4 | | vp |
. . . . . . . 8
setvar π |
5 | 4 | cv 1538 |
. . . . . . 7
class π |
6 | | cdgr 25936 |
. . . . . . 7
class
deg |
7 | 5, 6 | cfv 6542 |
. . . . . 6
class
(degβπ) |
8 | 2 | cv 1538 |
. . . . . . 7
class π₯ |
9 | | cdgraa 42184 |
. . . . . . 7
class
degAA |
10 | 8, 9 | cfv 6542 |
. . . . . 6
class
(degAAβπ₯) |
11 | 7, 10 | wceq 1539 |
. . . . 5
wff
(degβπ) =
(degAAβπ₯) |
12 | 8, 5 | cfv 6542 |
. . . . . 6
class (πβπ₯) |
13 | | cc0 11112 |
. . . . . 6
class
0 |
14 | 12, 13 | wceq 1539 |
. . . . 5
wff (πβπ₯) = 0 |
15 | | ccoe 25935 |
. . . . . . . 8
class
coeff |
16 | 5, 15 | cfv 6542 |
. . . . . . 7
class
(coeffβπ) |
17 | 10, 16 | cfv 6542 |
. . . . . 6
class
((coeffβπ)β(degAAβπ₯)) |
18 | | c1 11113 |
. . . . . 6
class
1 |
19 | 17, 18 | wceq 1539 |
. . . . 5
wff
((coeffβπ)β(degAAβπ₯)) = 1 |
20 | 11, 14, 19 | w3a 1085 |
. . . 4
wff
((degβπ) =
(degAAβπ₯)
β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1) |
21 | | cq 12936 |
. . . . 5
class
β |
22 | | cply 25933 |
. . . . 5
class
Poly |
23 | 21, 22 | cfv 6542 |
. . . 4
class
(Polyββ) |
24 | 20, 4, 23 | crio 7366 |
. . 3
class
(β©π
β (Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1)) |
25 | 2, 3, 24 | cmpt 5230 |
. 2
class (π₯ β πΈ β¦
(β©π β
(Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1))) |
26 | 1, 25 | wceq 1539 |
1
wff minPolyAA =
(π₯ β πΈ β¦
(β©π β
(Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1))) |