Step | Hyp | Ref
| Expression |
1 | | cldgis 41477 |
. 2
class
ldgIdlSeq |
2 | | vr |
. . 3
setvar π |
3 | | cvv 3448 |
. . 3
class
V |
4 | | vi |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . . 6
class π |
6 | | cpl1 21564 |
. . . . . 6
class
Poly1 |
7 | 5, 6 | cfv 6501 |
. . . . 5
class
(Poly1βπ) |
8 | | clidl 20647 |
. . . . 5
class
LIdeal |
9 | 7, 8 | cfv 6501 |
. . . 4
class
(LIdealβ(Poly1βπ)) |
10 | | vx |
. . . . 5
setvar π₯ |
11 | | cn0 12420 |
. . . . 5
class
β0 |
12 | | vk |
. . . . . . . . . . 11
setvar π |
13 | 12 | cv 1541 |
. . . . . . . . . 10
class π |
14 | | cdg1 25432 |
. . . . . . . . . . 11
class
deg1 |
15 | 5, 14 | cfv 6501 |
. . . . . . . . . 10
class (
deg1 βπ) |
16 | 13, 15 | cfv 6501 |
. . . . . . . . 9
class ((
deg1 βπ)βπ) |
17 | 10 | cv 1541 |
. . . . . . . . 9
class π₯ |
18 | | cle 11197 |
. . . . . . . . 9
class
β€ |
19 | 16, 17, 18 | wbr 5110 |
. . . . . . . 8
wff ((
deg1 βπ)βπ) β€ π₯ |
20 | | vj |
. . . . . . . . . 10
setvar π |
21 | 20 | cv 1541 |
. . . . . . . . 9
class π |
22 | | cco1 21565 |
. . . . . . . . . . 11
class
coe1 |
23 | 13, 22 | cfv 6501 |
. . . . . . . . . 10
class
(coe1βπ) |
24 | 17, 23 | cfv 6501 |
. . . . . . . . 9
class
((coe1βπ)βπ₯) |
25 | 21, 24 | wceq 1542 |
. . . . . . . 8
wff π = ((coe1βπ)βπ₯) |
26 | 19, 25 | wa 397 |
. . . . . . 7
wff (((
deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)) |
27 | 4 | cv 1541 |
. . . . . . 7
class π |
28 | 26, 12, 27 | wrex 3074 |
. . . . . 6
wff
βπ β
π ((( deg1
βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)) |
29 | 28, 20 | cab 2714 |
. . . . 5
class {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))} |
30 | 10, 11, 29 | cmpt 5193 |
. . . 4
class (π₯ β β0
β¦ {π β£
βπ β π ((( deg1
βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}) |
31 | 4, 9, 30 | cmpt 5193 |
. . 3
class (π β
(LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})) |
32 | 2, 3, 31 | cmpt 5193 |
. 2
class (π β V β¦ (π β
(LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) |
33 | 1, 32 | wceq 1542 |
1
wff ldgIdlSeq =
(π β V β¦ (π β
(LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) |