Step | Hyp | Ref
| Expression |
1 | | crngorngo 36488 |
. . . 4
β’ (π
β CRingOps β π
β
RingOps) |
2 | | eldifi 4091 |
. . . . 5
β’ (π΄ β (π β π) β π΄ β π) |
3 | | eldifi 4091 |
. . . . 5
β’ (π΅ β (π β π) β π΅ β π) |
4 | 2, 3 | anim12i 614 |
. . . 4
β’ ((π΄ β (π β π) β§ π΅ β (π β π)) β (π΄ β π β§ π΅ β π)) |
5 | | ispridlc.1 |
. . . . . 6
β’ πΊ = (1st βπ
) |
6 | | ispridlc.2 |
. . . . . 6
β’ π» = (2nd βπ
) |
7 | | ispridlc.3 |
. . . . . 6
β’ π = ran πΊ |
8 | 5, 6, 7 | rngocl 36389 |
. . . . 5
β’ ((π
β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π»π΅) β π) |
9 | 8 | 3expb 1121 |
. . . 4
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π)) β (π΄π»π΅) β π) |
10 | 1, 4, 9 | syl2an 597 |
. . 3
β’ ((π
β CRingOps β§ (π΄ β (π β π) β§ π΅ β (π β π))) β (π΄π»π΅) β π) |
11 | 10 | adantlr 714 |
. 2
β’ (((π
β CRingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (π β π) β§ π΅ β (π β π))) β (π΄π»π΅) β π) |
12 | | eldifn 4092 |
. . . 4
β’ (π΅ β (π β π) β Β¬ π΅ β π) |
13 | 12 | ad2antll 728 |
. . 3
β’ (((π
β CRingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (π β π) β§ π΅ β (π β π))) β Β¬ π΅ β π) |
14 | 5, 6, 7 | pridlc2 36560 |
. . . . . . 7
β’ (((π
β CRingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (π β π) β§ π΅ β π β§ (π΄π»π΅) β π)) β π΅ β π) |
15 | 14 | 3exp2 1355 |
. . . . . 6
β’ ((π
β CRingOps β§ π β (PrIdlβπ
)) β (π΄ β (π β π) β (π΅ β π β ((π΄π»π΅) β π β π΅ β π)))) |
16 | 15 | imp32 420 |
. . . . 5
β’ (((π
β CRingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (π β π) β§ π΅ β π)) β ((π΄π»π΅) β π β π΅ β π)) |
17 | 16 | con3d 152 |
. . . 4
β’ (((π
β CRingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (π β π) β§ π΅ β π)) β (Β¬ π΅ β π β Β¬ (π΄π»π΅) β π)) |
18 | 3, 17 | sylanr2 682 |
. . 3
β’ (((π
β CRingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (π β π) β§ π΅ β (π β π))) β (Β¬ π΅ β π β Β¬ (π΄π»π΅) β π)) |
19 | 13, 18 | mpd 15 |
. 2
β’ (((π
β CRingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (π β π) β§ π΅ β (π β π))) β Β¬ (π΄π»π΅) β π) |
20 | 11, 19 | eldifd 3926 |
1
β’ (((π
β CRingOps β§ π β (PrIdlβπ
)) β§ (π΄ β (π β π) β§ π΅ β (π β π))) β (π΄π»π΅) β (π β π)) |