Step | Hyp | Ref
| Expression |
1 | | eldif 3958 |
. . 3
β’ (π β (π΅ β π) β (π β π΅ β§ Β¬ π β π)) |
2 | | eldif 3958 |
. . . . . . . . 9
β’ (π₯ β (π΅ β π) β (π₯ β π΅ β§ Β¬ π₯ β π)) |
3 | | eldif 3958 |
. . . . . . . . 9
β’ (π¦ β (π΅ β π) β (π¦ β π΅ β§ Β¬ π¦ β π)) |
4 | 2, 3 | anbi12i 627 |
. . . . . . . 8
β’ ((π₯ β (π΅ β π) β§ π¦ β (π΅ β π)) β ((π₯ β π΅ β§ Β¬ π₯ β π) β§ (π¦ β π΅ β§ Β¬ π¦ β π))) |
5 | | an4 654 |
. . . . . . . 8
β’ (((π₯ β π΅ β§ Β¬ π₯ β π) β§ (π¦ β π΅ β§ Β¬ π¦ β π)) β ((π₯ β π΅ β§ π¦ β π΅) β§ (Β¬ π₯ β π β§ Β¬ π¦ β π))) |
6 | 4, 5 | bitri 274 |
. . . . . . 7
β’ ((π₯ β (π΅ β π) β§ π¦ β (π΅ β π)) β ((π₯ β π΅ β§ π¦ β π΅) β§ (Β¬ π₯ β π β§ Β¬ π¦ β π))) |
7 | 6 | imbi1i 349 |
. . . . . 6
β’ (((π₯ β (π΅ β π) β§ π¦ β (π΅ β π)) β (π₯ Β· π¦) β π) β (((π₯ β π΅ β§ π¦ β π΅) β§ (Β¬ π₯ β π β§ Β¬ π¦ β π)) β (π₯ Β· π¦) β π)) |
8 | | impexp 451 |
. . . . . . 7
β’ ((((π₯ β π΅ β§ π¦ β π΅) β§ (Β¬ π₯ β π β§ Β¬ π¦ β π)) β (π₯ Β· π¦) β π) β ((π₯ β π΅ β§ π¦ β π΅) β ((Β¬ π₯ β π β§ Β¬ π¦ β π) β (π₯ Β· π¦) β π))) |
9 | | pm4.56 987 |
. . . . . . . . . 10
β’ ((Β¬
π₯ β π β§ Β¬ π¦ β π) β Β¬ (π₯ β π β¨ π¦ β π)) |
10 | | df-ne 2941 |
. . . . . . . . . 10
β’ ((π₯ Β· π¦) β π β Β¬ (π₯ Β· π¦) = π) |
11 | 9, 10 | imbi12i 350 |
. . . . . . . . 9
β’ (((Β¬
π₯ β π β§ Β¬ π¦ β π) β (π₯ Β· π¦) β π) β (Β¬ (π₯ β π β¨ π¦ β π) β Β¬ (π₯ Β· π¦) = π)) |
12 | | con34b 315 |
. . . . . . . . 9
β’ (((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)) β (Β¬ (π₯ β π β¨ π¦ β π) β Β¬ (π₯ Β· π¦) = π)) |
13 | 11, 12 | bitr4i 277 |
. . . . . . . 8
β’ (((Β¬
π₯ β π β§ Β¬ π¦ β π) β (π₯ Β· π¦) β π) β ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π))) |
14 | 13 | imbi2i 335 |
. . . . . . 7
β’ (((π₯ β π΅ β§ π¦ β π΅) β ((Β¬ π₯ β π β§ Β¬ π¦ β π) β (π₯ Β· π¦) β π)) β ((π₯ β π΅ β§ π¦ β π΅) β ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) |
15 | 8, 14 | bitri 274 |
. . . . . 6
β’ ((((π₯ β π΅ β§ π¦ β π΅) β§ (Β¬ π₯ β π β§ Β¬ π¦ β π)) β (π₯ Β· π¦) β π) β ((π₯ β π΅ β§ π¦ β π΅) β ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) |
16 | 7, 15 | bitri 274 |
. . . . 5
β’ (((π₯ β (π΅ β π) β§ π¦ β (π΅ β π)) β (π₯ Β· π¦) β π) β ((π₯ β π΅ β§ π¦ β π΅) β ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) |
17 | 16 | 2albii 1822 |
. . . 4
β’
(βπ₯βπ¦((π₯ β (π΅ β π) β§ π¦ β (π΅ β π)) β (π₯ Β· π¦) β π) β βπ₯βπ¦((π₯ β π΅ β§ π¦ β π΅) β ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) |
18 | | r2al 3194 |
. . . 4
β’
(βπ₯ β
(π΅ β π)βπ¦ β (π΅ β π)(π₯ Β· π¦) β π β βπ₯βπ¦((π₯ β (π΅ β π) β§ π¦ β (π΅ β π)) β (π₯ Β· π¦) β π)) |
19 | | r2al 3194 |
. . . 4
β’
(βπ₯ β
π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)) β βπ₯βπ¦((π₯ β π΅ β§ π¦ β π΅) β ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) |
20 | 17, 18, 19 | 3bitr4i 302 |
. . 3
β’
(βπ₯ β
(π΅ β π)βπ¦ β (π΅ β π)(π₯ Β· π¦) β π β βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π))) |
21 | 1, 20 | anbi12i 627 |
. 2
β’ ((π β (π΅ β π) β§ βπ₯ β (π΅ β π)βπ¦ β (π΅ β π)(π₯ Β· π¦) β π) β ((π β π΅ β§ Β¬ π β π) β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) |
22 | | isirred2.1 |
. . 3
β’ π΅ = (Baseβπ
) |
23 | | isirred2.2 |
. . 3
β’ π = (Unitβπ
) |
24 | | isirred2.3 |
. . 3
β’ πΌ = (Irredβπ
) |
25 | | eqid 2732 |
. . 3
β’ (π΅ β π) = (π΅ β π) |
26 | | isirred2.4 |
. . 3
β’ Β· =
(.rβπ
) |
27 | 22, 23, 24, 25, 26 | isirred 20237 |
. 2
β’ (π β πΌ β (π β (π΅ β π) β§ βπ₯ β (π΅ β π)βπ¦ β (π΅ β π)(π₯ Β· π¦) β π)) |
28 | | df-3an 1089 |
. 2
β’ ((π β π΅ β§ Β¬ π β π β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π))) β ((π β π΅ β§ Β¬ π β π) β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) |
29 | 21, 27, 28 | 3bitr4i 302 |
1
β’ (π β πΌ β (π β π΅ β§ Β¬ π β π β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π β (π₯ β π β¨ π¦ β π)))) |