Step | Hyp | Ref
| Expression |
1 | | prmidlval.1 |
. . . . 5
β’ π΅ = (Baseβπ
) |
2 | | prmidlval.2 |
. . . . 5
β’ Β· =
(.rβπ
) |
3 | 1, 2 | prmidlval 32257 |
. . . 4
β’ (π
β Ring β
(PrmIdealβπ
) = {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))}) |
4 | 3 | eleq2d 2820 |
. . 3
β’ (π
β Ring β (π β (PrmIdealβπ
) β π β {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))})) |
5 | | neeq1 3003 |
. . . . 5
β’ (π = π β (π β π΅ β π β π΅)) |
6 | | eleq2 2823 |
. . . . . . . 8
β’ (π = π β ((π₯ Β· π¦) β π β (π₯ Β· π¦) β π)) |
7 | 6 | 2ralbidv 3209 |
. . . . . . 7
β’ (π = π β (βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π)) |
8 | | sseq2 3971 |
. . . . . . . 8
β’ (π = π β (π β π β π β π)) |
9 | | sseq2 3971 |
. . . . . . . 8
β’ (π = π β (π β π β π β π)) |
10 | 8, 9 | orbi12d 918 |
. . . . . . 7
β’ (π = π β ((π β π β¨ π β π) β (π β π β¨ π β π))) |
11 | 7, 10 | imbi12d 345 |
. . . . . 6
β’ (π = π β ((βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)) β (βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))) |
12 | 11 | 2ralbidv 3209 |
. . . . 5
β’ (π = π β (βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)) β βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))) |
13 | 5, 12 | anbi12d 632 |
. . . 4
β’ (π = π β ((π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))) β (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))))) |
14 | 13 | elrab 3646 |
. . 3
β’ (π β {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))} β (π β (LIdealβπ
) β§ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))))) |
15 | 4, 14 | bitrdi 287 |
. 2
β’ (π
β Ring β (π β (PrmIdealβπ
) β (π β (LIdealβπ
) β§ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))))) |
16 | | 3anass 1096 |
. 2
β’ ((π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))) β (π β (LIdealβπ
) β§ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))))) |
17 | 15, 16 | bitr4di 289 |
1
β’ (π
β Ring β (π β (PrmIdealβπ
) β (π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))))) |