Step | Hyp | Ref
| Expression |
1 | | mxidlval.1 |
. . . 4
β’ π΅ = (Baseβπ
) |
2 | 1 | mxidlval 32230 |
. . 3
β’ (π
β Ring β
(MaxIdealβπ
) = {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))}) |
3 | 2 | eleq2d 2823 |
. 2
β’ (π
β Ring β (π β (MaxIdealβπ
) β π β {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))})) |
4 | | neeq1 3006 |
. . . . 5
β’ (π = π β (π β π΅ β π β π΅)) |
5 | | sseq1 3969 |
. . . . . . 7
β’ (π = π β (π β π β π β π)) |
6 | | eqeq2 2748 |
. . . . . . . 8
β’ (π = π β (π = π β π = π)) |
7 | 6 | orbi1d 915 |
. . . . . . 7
β’ (π = π β ((π = π β¨ π = π΅) β (π = π β¨ π = π΅))) |
8 | 5, 7 | imbi12d 344 |
. . . . . 6
β’ (π = π β ((π β π β (π = π β¨ π = π΅)) β (π β π β (π = π β¨ π = π΅)))) |
9 | 8 | ralbidv 3174 |
. . . . 5
β’ (π = π β (βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)) β βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))) |
10 | 4, 9 | anbi12d 631 |
. . . 4
β’ (π = π β ((π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))) β (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))))) |
11 | 10 | elrab 3645 |
. . 3
β’ (π β {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))} β (π β (LIdealβπ
) β§ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))))) |
12 | | 3anass 1095 |
. . 3
β’ ((π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))) β (π β (LIdealβπ
) β§ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))))) |
13 | 11, 12 | bitr4i 277 |
. 2
β’ (π β {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))} β (π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))) |
14 | 3, 13 | bitrdi 286 |
1
β’ (π
β Ring β (π β (MaxIdealβπ
) β (π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))))) |