Step | Hyp | Ref
| Expression |
1 | | sseq2 3974 |
. . . 4
β’ (π = πΌ β (π β π β π β πΌ)) |
2 | | eqeq1 2737 |
. . . . 5
β’ (π = πΌ β (π = π β πΌ = π)) |
3 | | eqeq1 2737 |
. . . . 5
β’ (π = πΌ β (π = π΅ β πΌ = π΅)) |
4 | 2, 3 | orbi12d 918 |
. . . 4
β’ (π = πΌ β ((π = π β¨ π = π΅) β (πΌ = π β¨ πΌ = π΅))) |
5 | 1, 4 | imbi12d 345 |
. . 3
β’ (π = πΌ β ((π β π β (π = π β¨ π = π΅)) β (π β πΌ β (πΌ = π β¨ πΌ = π΅)))) |
6 | | mxidlval.1 |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
7 | 6 | ismxidl 32286 |
. . . . . 6
β’ (π
β Ring β (π β (MaxIdealβπ
) β (π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))))) |
8 | 7 | biimpa 478 |
. . . . 5
β’ ((π
β Ring β§ π β (MaxIdealβπ
)) β (π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅)))) |
9 | 8 | simp3d 1145 |
. . . 4
β’ ((π
β Ring β§ π β (MaxIdealβπ
)) β βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))) |
10 | 9 | adantr 482 |
. . 3
β’ (((π
β Ring β§ π β (MaxIdealβπ
)) β§ πΌ β (LIdealβπ
)) β βπ β (LIdealβπ
)(π β π β (π = π β¨ π = π΅))) |
11 | | simpr 486 |
. . 3
β’ (((π
β Ring β§ π β (MaxIdealβπ
)) β§ πΌ β (LIdealβπ
)) β πΌ β (LIdealβπ
)) |
12 | 5, 10, 11 | rspcdva 3584 |
. 2
β’ (((π
β Ring β§ π β (MaxIdealβπ
)) β§ πΌ β (LIdealβπ
)) β (π β πΌ β (πΌ = π β¨ πΌ = π΅))) |
13 | 12 | impr 456 |
1
β’ (((π
β Ring β§ π β (MaxIdealβπ
)) β§ (πΌ β (LIdealβπ
) β§ π β πΌ)) β (πΌ = π β¨ πΌ = π΅)) |