Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . 7
β’
(1st βπ
) = (1st βπ
) |
2 | | pridl.1 |
. . . . . . 7
β’ π» = (2nd βπ
) |
3 | | eqid 2737 |
. . . . . . 7
β’ ran
(1st βπ
) =
ran (1st βπ
) |
4 | 1, 2, 3 | ispridl 36496 |
. . . . . 6
β’ (π
β RingOps β (π β (PrIdlβπ
) β (π β (Idlβπ
) β§ π β ran (1st βπ
) β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π))))) |
5 | | df-3an 1090 |
. . . . . 6
β’ ((π β (Idlβπ
) β§ π β ran (1st βπ
) β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π))) β ((π β (Idlβπ
) β§ π β ran (1st βπ
)) β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)))) |
6 | 4, 5 | bitrdi 287 |
. . . . 5
β’ (π
β RingOps β (π β (PrIdlβπ
) β ((π β (Idlβπ
) β§ π β ran (1st βπ
)) β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π))))) |
7 | 6 | simplbda 501 |
. . . 4
β’ ((π
β RingOps β§ π β (PrIdlβπ
)) β βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π))) |
8 | | raleq 3310 |
. . . . . 6
β’ (π = π΄ β (βπ₯ β π βπ¦ β π (π₯π»π¦) β π β βπ₯ β π΄ βπ¦ β π (π₯π»π¦) β π)) |
9 | | sseq1 3970 |
. . . . . . 7
β’ (π = π΄ β (π β π β π΄ β π)) |
10 | 9 | orbi1d 916 |
. . . . . 6
β’ (π = π΄ β ((π β π β¨ π β π) β (π΄ β π β¨ π β π))) |
11 | 8, 10 | imbi12d 345 |
. . . . 5
β’ (π = π΄ β ((βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)) β (βπ₯ β π΄ βπ¦ β π (π₯π»π¦) β π β (π΄ β π β¨ π β π)))) |
12 | | raleq 3310 |
. . . . . . 7
β’ (π = π΅ β (βπ¦ β π (π₯π»π¦) β π β βπ¦ β π΅ (π₯π»π¦) β π)) |
13 | 12 | ralbidv 3175 |
. . . . . 6
β’ (π = π΅ β (βπ₯ β π΄ βπ¦ β π (π₯π»π¦) β π β βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π)) |
14 | | sseq1 3970 |
. . . . . . 7
β’ (π = π΅ β (π β π β π΅ β π)) |
15 | 14 | orbi2d 915 |
. . . . . 6
β’ (π = π΅ β ((π΄ β π β¨ π β π) β (π΄ β π β¨ π΅ β π))) |
16 | 13, 15 | imbi12d 345 |
. . . . 5
β’ (π = π΅ β ((βπ₯ β π΄ βπ¦ β π (π₯π»π¦) β π β (π΄ β π β¨ π β π)) β (βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π β (π΄ β π β¨ π΅ β π)))) |
17 | 11, 16 | rspc2v 3591 |
. . . 4
β’ ((π΄ β (Idlβπ
) β§ π΅ β (Idlβπ
)) β (βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)) β (βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π β (π΄ β π β¨ π΅ β π)))) |
18 | 7, 17 | syl5com 31 |
. . 3
β’ ((π
β RingOps β§ π β (PrIdlβπ
)) β ((π΄ β (Idlβπ
) β§ π΅ β (Idlβπ
)) β (βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π β (π΄ β π β¨ π΅ β π)))) |
19 | 18 | expd 417 |
. 2
β’ ((π
β RingOps β§ π β (PrIdlβπ
)) β (π΄ β (Idlβπ
) β (π΅ β (Idlβπ
) β (βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π β (π΄ β π β¨ π΅ β π))))) |
20 | 19 | 3imp2 1350 |
1
β’ (((π
β RingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (Idlβπ
) β§ π΅ β (Idlβπ
) β§ βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π)) β (π΄ β π β¨ π΅ β π)) |