Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . 3
β’ (π = π
β (LIdealβπ) = (LIdealβπ
)) |
2 | | fveq2 6846 |
. . . . . 6
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
3 | | mxidlval.1 |
. . . . . 6
β’ π΅ = (Baseβπ
) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π = π
β (Baseβπ) = π΅) |
5 | 4 | neeq2d 3001 |
. . . 4
β’ (π = π
β (π β (Baseβπ) β π β π΅)) |
6 | 4 | eqeq2d 2744 |
. . . . . . 7
β’ (π = π
β (π = (Baseβπ) β π = π΅)) |
7 | 6 | orbi2d 915 |
. . . . . 6
β’ (π = π
β ((π = π β¨ π = (Baseβπ)) β (π = π β¨ π = π΅))) |
8 | 7 | imbi2d 341 |
. . . . 5
β’ (π = π
β ((π β π β (π = π β¨ π = (Baseβπ))) β (π β π β (π = π β¨ π = π΅)))) |
9 | 1, 8 | raleqbidv 3318 |
. . . 4
β’ (π = π
β (βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ))) β βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))) |
10 | 5, 9 | anbi12d 632 |
. . 3
β’ (π = π
β ((π β (Baseβπ) β§ βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ)))) β (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))))) |
11 | 1, 10 | rabeqbidv 3423 |
. 2
β’ (π = π
β {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ))))} = {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))}) |
12 | | df-mxidl 32284 |
. 2
β’ MaxIdeal
= (π β Ring β¦
{π β
(LIdealβπ) β£
(π β (Baseβπ) β§ βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ))))}) |
13 | | fvex 6859 |
. . 3
β’
(LIdealβπ
)
β V |
14 | 13 | rabex 5293 |
. 2
β’ {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))} β V |
15 | 11, 12, 14 | fvmpt 6952 |
1
β’ (π
β Ring β
(MaxIdealβπ
) = {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))}) |