Step | Hyp | Ref
| Expression |
1 | | raleq 3308 |
. . . . 5
β’ (π = π½ β (βπ¦ β π (π₯ Β· π¦) β π β βπ¦ β π½ (π₯ Β· π¦) β π)) |
2 | 1 | ralbidv 3171 |
. . . 4
β’ (π = π½ β (βπ₯ β πΌ βπ¦ β π (π₯ Β· π¦) β π β βπ₯ β πΌ βπ¦ β π½ (π₯ Β· π¦) β π)) |
3 | | sseq1 3970 |
. . . . 5
β’ (π = π½ β (π β π β π½ β π)) |
4 | 3 | orbi2d 915 |
. . . 4
β’ (π = π½ β ((πΌ β π β¨ π β π) β (πΌ β π β¨ π½ β π))) |
5 | 2, 4 | imbi12d 345 |
. . 3
β’ (π = π½ β ((βπ₯ β πΌ βπ¦ β π (π₯ Β· π¦) β π β (πΌ β π β¨ π β π)) β (βπ₯ β πΌ βπ¦ β π½ (π₯ Β· π¦) β π β (πΌ β π β¨ π½ β π)))) |
6 | | raleq 3308 |
. . . . . 6
β’ (π = πΌ β (βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β βπ₯ β πΌ βπ¦ β π (π₯ Β· π¦) β π)) |
7 | | sseq1 3970 |
. . . . . . 7
β’ (π = πΌ β (π β π β πΌ β π)) |
8 | 7 | orbi1d 916 |
. . . . . 6
β’ (π = πΌ β ((π β π β¨ π β π) β (πΌ β π β¨ π β π))) |
9 | 6, 8 | imbi12d 345 |
. . . . 5
β’ (π = πΌ β ((βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)) β (βπ₯ β πΌ βπ¦ β π (π₯ Β· π¦) β π β (πΌ β π β¨ π β π)))) |
10 | 9 | ralbidv 3171 |
. . . 4
β’ (π = πΌ β (βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)) β βπ β (LIdealβπ
)(βπ₯ β πΌ βπ¦ β π (π₯ Β· π¦) β π β (πΌ β π β¨ π β π)))) |
11 | | prmidlval.1 |
. . . . . . . 8
β’ π΅ = (Baseβπ
) |
12 | | prmidlval.2 |
. . . . . . . 8
β’ Β· =
(.rβπ
) |
13 | 11, 12 | isprmidl 32258 |
. . . . . . 7
β’ (π
β Ring β (π β (PrmIdealβπ
) β (π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))))) |
14 | 13 | biimpa 478 |
. . . . . 6
β’ ((π
β Ring β§ π β (PrmIdealβπ
)) β (π β (LIdealβπ
) β§ π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))) |
15 | 14 | simp3d 1145 |
. . . . 5
β’ ((π
β Ring β§ π β (PrmIdealβπ
)) β βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))) |
16 | 15 | adantr 482 |
. . . 4
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ (πΌ β (LIdealβπ
) β§ π½ β (LIdealβπ
))) β βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))) |
17 | | simprl 770 |
. . . 4
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ (πΌ β (LIdealβπ
) β§ π½ β (LIdealβπ
))) β πΌ β (LIdealβπ
)) |
18 | 10, 16, 17 | rspcdva 3581 |
. . 3
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ (πΌ β (LIdealβπ
) β§ π½ β (LIdealβπ
))) β βπ β (LIdealβπ
)(βπ₯ β πΌ βπ¦ β π (π₯ Β· π¦) β π β (πΌ β π β¨ π β π))) |
19 | | simprr 772 |
. . 3
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ (πΌ β (LIdealβπ
) β§ π½ β (LIdealβπ
))) β π½ β (LIdealβπ
)) |
20 | 5, 18, 19 | rspcdva 3581 |
. 2
β’ (((π
β Ring β§ π β (PrmIdealβπ
)) β§ (πΌ β (LIdealβπ
) β§ π½ β (LIdealβπ
))) β (βπ₯ β πΌ βπ¦ β π½ (π₯ Β· π¦) β π β (πΌ β π β¨ π½ β π))) |
21 | 20 | imp 408 |
1
β’ ((((π
β Ring β§ π β (PrmIdealβπ
)) β§ (πΌ β (LIdealβπ
) β§ π½ β (LIdealβπ
))) β§ βπ₯ β πΌ βπ¦ β π½ (π₯ Β· π¦) β π) β (πΌ β π β¨ π½ β π)) |