Step | Hyp | Ref
| Expression |
1 | | clring 13262 |
. 2
class
LRing |
2 | | vx |
. . . . . . . . 9
setvar π₯ |
3 | 2 | cv 1352 |
. . . . . . . 8
class π₯ |
4 | | vy |
. . . . . . . . 9
setvar π¦ |
5 | 4 | cv 1352 |
. . . . . . . 8
class π¦ |
6 | | vr |
. . . . . . . . . 10
setvar π |
7 | 6 | cv 1352 |
. . . . . . . . 9
class π |
8 | | cplusg 12528 |
. . . . . . . . 9
class
+g |
9 | 7, 8 | cfv 5215 |
. . . . . . . 8
class
(+gβπ) |
10 | 3, 5, 9 | co 5872 |
. . . . . . 7
class (π₯(+gβπ)π¦) |
11 | | cur 13073 |
. . . . . . . 8
class
1r |
12 | 7, 11 | cfv 5215 |
. . . . . . 7
class
(1rβπ) |
13 | 10, 12 | wceq 1353 |
. . . . . 6
wff (π₯(+gβπ)π¦) = (1rβπ) |
14 | | cui 13187 |
. . . . . . . . 9
class
Unit |
15 | 7, 14 | cfv 5215 |
. . . . . . . 8
class
(Unitβπ) |
16 | 3, 15 | wcel 2148 |
. . . . . . 7
wff π₯ β (Unitβπ) |
17 | 5, 15 | wcel 2148 |
. . . . . . 7
wff π¦ β (Unitβπ) |
18 | 16, 17 | wo 708 |
. . . . . 6
wff (π₯ β (Unitβπ) β¨ π¦ β (Unitβπ)) |
19 | 13, 18 | wi 4 |
. . . . 5
wff ((π₯(+gβπ)π¦) = (1rβπ) β (π₯ β (Unitβπ) β¨ π¦ β (Unitβπ))) |
20 | | cbs 12454 |
. . . . . 6
class
Base |
21 | 7, 20 | cfv 5215 |
. . . . 5
class
(Baseβπ) |
22 | 19, 4, 21 | wral 2455 |
. . . 4
wff
βπ¦ β
(Baseβπ)((π₯(+gβπ)π¦) = (1rβπ) β (π₯ β (Unitβπ) β¨ π¦ β (Unitβπ))) |
23 | 22, 2, 21 | wral 2455 |
. . 3
wff
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = (1rβπ) β (π₯ β (Unitβπ) β¨ π¦ β (Unitβπ))) |
24 | | cnzr 13254 |
. . 3
class
NzRing |
25 | 23, 6, 24 | crab 2459 |
. 2
class {π β NzRing β£
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = (1rβπ) β (π₯ β (Unitβπ) β¨ π¦ β (Unitβπ)))} |
26 | 1, 25 | wceq 1353 |
1
wff LRing =
{π β NzRing β£
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((π₯(+gβπ)π¦) = (1rβπ) β (π₯ β (Unitβπ) β¨ π¦ β (Unitβπ)))} |