Step | Hyp | Ref
| Expression |
1 | | clpidl 20727 |
. 2
class
LPIdeal |
2 | | vw |
. . 3
setvar π€ |
3 | | crg 19969 |
. . 3
class
Ring |
4 | | vg |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . 5
class π€ |
6 | | cbs 17088 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6497 |
. . . 4
class
(Baseβπ€) |
8 | 4 | cv 1541 |
. . . . . . 7
class π |
9 | 8 | csn 4587 |
. . . . . 6
class {π} |
10 | | crsp 20648 |
. . . . . . 7
class
RSpan |
11 | 5, 10 | cfv 6497 |
. . . . . 6
class
(RSpanβπ€) |
12 | 9, 11 | cfv 6497 |
. . . . 5
class
((RSpanβπ€)β{π}) |
13 | 12 | csn 4587 |
. . . 4
class
{((RSpanβπ€)β{π})} |
14 | 4, 7, 13 | ciun 4955 |
. . 3
class βͺ π β (Baseβπ€){((RSpanβπ€)β{π})} |
15 | 2, 3, 14 | cmpt 5189 |
. 2
class (π€ β Ring β¦ βͺ π β (Baseβπ€){((RSpanβπ€)β{π})}) |
16 | 1, 15 | wceq 1542 |
1
wff LPIdeal =
(π€ β Ring β¦
βͺ π β (Baseβπ€){((RSpanβπ€)β{π})}) |