Step | Hyp | Ref
| Expression |
1 | | irredmul.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
2 | | irredmul.u |
. . . . 5
β’ π = (Unitβπ
) |
3 | | irredn0.i |
. . . . 5
β’ πΌ = (Irredβπ
) |
4 | | irredmul.t |
. . . . 5
β’ Β· =
(.rβπ
) |
5 | 1, 2, 3, 4 | isirred2 20131 |
. . . 4
β’ ((π Β· π) β πΌ β ((π Β· π) β π΅ β§ Β¬ (π Β· π) β π β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = (π Β· π) β (π₯ β π β¨ π¦ β π)))) |
6 | 5 | simp3bi 1148 |
. . 3
β’ ((π Β· π) β πΌ β βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = (π Β· π) β (π₯ β π β¨ π¦ β π))) |
7 | | eqid 2737 |
. . . 4
β’ (π Β· π) = (π Β· π) |
8 | | oveq1 7365 |
. . . . . . 7
β’ (π₯ = π β (π₯ Β· π¦) = (π Β· π¦)) |
9 | 8 | eqeq1d 2739 |
. . . . . 6
β’ (π₯ = π β ((π₯ Β· π¦) = (π Β· π) β (π Β· π¦) = (π Β· π))) |
10 | | eleq1 2826 |
. . . . . . 7
β’ (π₯ = π β (π₯ β π β π β π)) |
11 | 10 | orbi1d 916 |
. . . . . 6
β’ (π₯ = π β ((π₯ β π β¨ π¦ β π) β (π β π β¨ π¦ β π))) |
12 | 9, 11 | imbi12d 345 |
. . . . 5
β’ (π₯ = π β (((π₯ Β· π¦) = (π Β· π) β (π₯ β π β¨ π¦ β π)) β ((π Β· π¦) = (π Β· π) β (π β π β¨ π¦ β π)))) |
13 | | oveq2 7366 |
. . . . . . 7
β’ (π¦ = π β (π Β· π¦) = (π Β· π)) |
14 | 13 | eqeq1d 2739 |
. . . . . 6
β’ (π¦ = π β ((π Β· π¦) = (π Β· π) β (π Β· π) = (π Β· π))) |
15 | | eleq1 2826 |
. . . . . . 7
β’ (π¦ = π β (π¦ β π β π β π)) |
16 | 15 | orbi2d 915 |
. . . . . 6
β’ (π¦ = π β ((π β π β¨ π¦ β π) β (π β π β¨ π β π))) |
17 | 14, 16 | imbi12d 345 |
. . . . 5
β’ (π¦ = π β (((π Β· π¦) = (π Β· π) β (π β π β¨ π¦ β π)) β ((π Β· π) = (π Β· π) β (π β π β¨ π β π)))) |
18 | 12, 17 | rspc2v 3591 |
. . . 4
β’ ((π β π΅ β§ π β π΅) β (βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = (π Β· π) β (π₯ β π β¨ π¦ β π)) β ((π Β· π) = (π Β· π) β (π β π β¨ π β π)))) |
19 | 7, 18 | mpii 46 |
. . 3
β’ ((π β π΅ β§ π β π΅) β (βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = (π Β· π) β (π₯ β π β¨ π¦ β π)) β (π β π β¨ π β π))) |
20 | 6, 19 | syl5 34 |
. 2
β’ ((π β π΅ β§ π β π΅) β ((π Β· π) β πΌ β (π β π β¨ π β π))) |
21 | 20 | 3impia 1118 |
1
β’ ((π β π΅ β§ π β π΅ β§ (π Β· π) β πΌ) β (π β π β¨ π β π)) |