Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . . 4
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π
β CRing) |
2 | | unitmulclb.1 |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
3 | 2 | a1i 9 |
. . . . . 6
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π΅ = (Baseβπ
)) |
4 | | eqid 2177 |
. . . . . . 7
β’
(β₯rβπ
) = (β₯rβπ
) |
5 | 4 | a1i 9 |
. . . . . 6
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β (β₯rβπ
) =
(β₯rβπ
)) |
6 | 1 | crngringd 13192 |
. . . . . . 7
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π
β Ring) |
7 | | ringsrg 13224 |
. . . . . . 7
β’ (π
β Ring β π
β SRing) |
8 | 6, 7 | syl 14 |
. . . . . 6
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π
β SRing) |
9 | | unitmulcl.2 |
. . . . . . 7
β’ Β· =
(.rβπ
) |
10 | 9 | a1i 9 |
. . . . . 6
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β Β· =
(.rβπ
)) |
11 | | simp2 998 |
. . . . . 6
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π β π΅) |
12 | | simp3 999 |
. . . . . 6
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π β π΅) |
13 | 3, 5, 8, 10, 11, 12 | dvdsrmuld 13265 |
. . . . 5
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π(β₯rβπ
)(π Β· π)) |
14 | 2, 9 | crngcom 13197 |
. . . . 5
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β (π Β· π) = (π Β· π)) |
15 | 13, 14 | breqtrrd 4032 |
. . . 4
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π(β₯rβπ
)(π Β· π)) |
16 | | unitmulcl.1 |
. . . . . 6
β’ π = (Unitβπ
) |
17 | 16, 4 | dvdsunit 13281 |
. . . . 5
β’ ((π
β CRing β§ π(β₯rβπ
)(π Β· π) β§ (π Β· π) β π) β π β π) |
18 | 17 | 3expia 1205 |
. . . 4
β’ ((π
β CRing β§ π(β₯rβπ
)(π Β· π)) β ((π Β· π) β π β π β π)) |
19 | 1, 15, 18 | syl2anc 411 |
. . 3
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β ((π Β· π) β π β π β π)) |
20 | 3, 5, 8, 10, 12, 11 | dvdsrmuld 13265 |
. . . 4
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π(β₯rβπ
)(π Β· π)) |
21 | 16, 4 | dvdsunit 13281 |
. . . . 5
β’ ((π
β CRing β§ π(β₯rβπ
)(π Β· π) β§ (π Β· π) β π) β π β π) |
22 | 21 | 3expia 1205 |
. . . 4
β’ ((π
β CRing β§ π(β₯rβπ
)(π Β· π)) β ((π Β· π) β π β π β π)) |
23 | 1, 20, 22 | syl2anc 411 |
. . 3
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β ((π Β· π) β π β π β π)) |
24 | 19, 23 | jcad 307 |
. 2
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β ((π Β· π) β π β (π β π β§ π β π))) |
25 | | crngring 13191 |
. . . 4
β’ (π
β CRing β π
β Ring) |
26 | 25 | 3ad2ant1 1018 |
. . 3
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β π
β Ring) |
27 | 16, 9 | unitmulcl 13282 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π) β π) |
28 | 27 | 3expib 1206 |
. . 3
β’ (π
β Ring β ((π β π β§ π β π) β (π Β· π) β π)) |
29 | 26, 28 | syl 14 |
. 2
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β ((π β π β§ π β π) β (π Β· π) β π)) |
30 | 24, 29 | impbid 129 |
1
β’ ((π
β CRing β§ π β π΅ β§ π β π΅) β ((π Β· π) β π β (π β π β§ π β π))) |