Step | Hyp | Ref
| Expression |
1 | | cprmidl 32255 |
. 2
class
PrmIdeal |
2 | | vr |
. . 3
setvar π |
3 | | crg 19969 |
. . 3
class
Ring |
4 | | vi |
. . . . . . 7
setvar π |
5 | 4 | cv 1541 |
. . . . . 6
class π |
6 | 2 | cv 1541 |
. . . . . . 7
class π |
7 | | cbs 17088 |
. . . . . . 7
class
Base |
8 | 6, 7 | cfv 6497 |
. . . . . 6
class
(Baseβπ) |
9 | 5, 8 | wne 2940 |
. . . . 5
wff π β (Baseβπ) |
10 | | vx |
. . . . . . . . . . . . 13
setvar π₯ |
11 | 10 | cv 1541 |
. . . . . . . . . . . 12
class π₯ |
12 | | vy |
. . . . . . . . . . . . 13
setvar π¦ |
13 | 12 | cv 1541 |
. . . . . . . . . . . 12
class π¦ |
14 | | cmulr 17139 |
. . . . . . . . . . . . 13
class
.r |
15 | 6, 14 | cfv 6497 |
. . . . . . . . . . . 12
class
(.rβπ) |
16 | 11, 13, 15 | co 7358 |
. . . . . . . . . . 11
class (π₯(.rβπ)π¦) |
17 | 16, 5 | wcel 2107 |
. . . . . . . . . 10
wff (π₯(.rβπ)π¦) β π |
18 | | vb |
. . . . . . . . . . 11
setvar π |
19 | 18 | cv 1541 |
. . . . . . . . . 10
class π |
20 | 17, 12, 19 | wral 3061 |
. . . . . . . . 9
wff
βπ¦ β
π (π₯(.rβπ)π¦) β π |
21 | | va |
. . . . . . . . . 10
setvar π |
22 | 21 | cv 1541 |
. . . . . . . . 9
class π |
23 | 20, 10, 22 | wral 3061 |
. . . . . . . 8
wff
βπ₯ β
π βπ¦ β π (π₯(.rβπ)π¦) β π |
24 | 22, 5 | wss 3911 |
. . . . . . . . 9
wff π β π |
25 | 19, 5 | wss 3911 |
. . . . . . . . 9
wff π β π |
26 | 24, 25 | wo 846 |
. . . . . . . 8
wff (π β π β¨ π β π) |
27 | 23, 26 | wi 4 |
. . . . . . 7
wff
(βπ₯ β
π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)) |
28 | | clidl 20647 |
. . . . . . . 8
class
LIdeal |
29 | 6, 28 | cfv 6497 |
. . . . . . 7
class
(LIdealβπ) |
30 | 27, 18, 29 | wral 3061 |
. . . . . 6
wff
βπ β
(LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)) |
31 | 30, 21, 29 | wral 3061 |
. . . . 5
wff
βπ β
(LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)) |
32 | 9, 31 | wa 397 |
. . . 4
wff (π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π))) |
33 | 32, 4, 29 | crab 3406 |
. . 3
class {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)))} |
34 | 2, 3, 33 | cmpt 5189 |
. 2
class (π β Ring β¦ {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)))}) |
35 | 1, 34 | wceq 1542 |
1
wff PrmIdeal =
(π β Ring β¦
{π β
(LIdealβπ) β£
(π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)))}) |