Step | Hyp | Ref
| Expression |
1 | | ornglmullt.1 |
. . . . 5
β’ (π β π
β oRing) |
2 | | orngogrp 32922 |
. . . . 5
β’ (π
β oRing β π
β oGrp) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π
β oGrp) |
4 | | isogrp 32726 |
. . . . 5
β’ (π
β oGrp β (π
β Grp β§ π
β oMnd)) |
5 | 4 | simprbi 496 |
. . . 4
β’ (π
β oGrp β π
β oMnd) |
6 | 3, 5 | syl 17 |
. . 3
β’ (π β π
β oMnd) |
7 | | orngring 32921 |
. . . . . 6
β’ (π
β oRing β π
β Ring) |
8 | 1, 7 | syl 17 |
. . . . 5
β’ (π β π
β Ring) |
9 | | ringgrp 20143 |
. . . . 5
β’ (π
β Ring β π
β Grp) |
10 | 8, 9 | syl 17 |
. . . 4
β’ (π β π
β Grp) |
11 | | ornglmullt.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
12 | | ornglmullt.0 |
. . . . 5
β’ 0 =
(0gβπ
) |
13 | 11, 12 | grpidcl 18895 |
. . . 4
β’ (π
β Grp β 0 β π΅) |
14 | 10, 13 | syl 17 |
. . 3
β’ (π β 0 β π΅) |
15 | | ornglmullt.4 |
. . . . 5
β’ (π β π β π΅) |
16 | | ornglmullt.3 |
. . . . 5
β’ (π β π β π΅) |
17 | | ornglmullt.t |
. . . . . 6
β’ Β· =
(.rβπ
) |
18 | 11, 17 | ringcl 20155 |
. . . . 5
β’ ((π
β Ring β§ π β π΅ β§ π β π΅) β (π Β· π) β π΅) |
19 | 8, 15, 16, 18 | syl3anc 1368 |
. . . 4
β’ (π β (π Β· π) β π΅) |
20 | | ornglmullt.2 |
. . . . 5
β’ (π β π β π΅) |
21 | 11, 17 | ringcl 20155 |
. . . . 5
β’ ((π
β Ring β§ π β π΅ β§ π β π΅) β (π Β· π) β π΅) |
22 | 8, 15, 20, 21 | syl3anc 1368 |
. . . 4
β’ (π β (π Β· π) β π΅) |
23 | | eqid 2726 |
. . . . 5
β’
(-gβπ
) = (-gβπ
) |
24 | 11, 23 | grpsubcl 18948 |
. . . 4
β’ ((π
β Grp β§ (π Β· π) β π΅ β§ (π Β· π) β π΅) β ((π Β· π)(-gβπ
)(π Β· π)) β π΅) |
25 | 10, 19, 22, 24 | syl3anc 1368 |
. . 3
β’ (π β ((π Β· π)(-gβπ
)(π Β· π)) β π΅) |
26 | | orngmulle.6 |
. . . . 5
β’ (π β 0 β€ π) |
27 | 11, 23 | grpsubcl 18948 |
. . . . . 6
β’ ((π
β Grp β§ π β π΅ β§ π β π΅) β (π(-gβπ
)π) β π΅) |
28 | 10, 16, 20, 27 | syl3anc 1368 |
. . . . 5
β’ (π β (π(-gβπ
)π) β π΅) |
29 | 11, 12, 23 | grpsubid 18952 |
. . . . . . 7
β’ ((π
β Grp β§ π β π΅) β (π(-gβπ
)π) = 0 ) |
30 | 10, 20, 29 | syl2anc 583 |
. . . . . 6
β’ (π β (π(-gβπ
)π) = 0 ) |
31 | | orngmulle.5 |
. . . . . . 7
β’ (π β π β€ π) |
32 | | orngmulle.l |
. . . . . . . 8
β’ β€ =
(leβπ
) |
33 | 11, 32, 23 | ogrpsub 32740 |
. . . . . . 7
β’ ((π
β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π(-gβπ
)π) β€ (π(-gβπ
)π)) |
34 | 3, 20, 16, 20, 31, 33 | syl131anc 1380 |
. . . . . 6
β’ (π β (π(-gβπ
)π) β€ (π(-gβπ
)π)) |
35 | 30, 34 | eqbrtrrd 5165 |
. . . . 5
β’ (π β 0 β€ (π(-gβπ
)π)) |
36 | 11, 32, 12, 17 | orngmul 32924 |
. . . . 5
β’ ((π
β oRing β§ (π β π΅ β§ 0 β€ π) β§ ((π(-gβπ
)π) β π΅ β§ 0 β€ (π(-gβπ
)π))) β 0 β€ (π Β· (π(-gβπ
)π))) |
37 | 1, 15, 26, 28, 35, 36 | syl122anc 1376 |
. . . 4
β’ (π β 0 β€ (π Β· (π(-gβπ
)π))) |
38 | 11, 17, 23, 8, 15, 16, 20 | ringsubdi 20206 |
. . . 4
β’ (π β (π Β· (π(-gβπ
)π)) = ((π Β· π)(-gβπ
)(π Β· π))) |
39 | 37, 38 | breqtrd 5167 |
. . 3
β’ (π β 0 β€ ((π Β· π)(-gβπ
)(π Β· π))) |
40 | | eqid 2726 |
. . . 4
β’
(+gβπ
) = (+gβπ
) |
41 | 11, 32, 40 | omndadd 32730 |
. . 3
β’ ((π
β oMnd β§ ( 0 β π΅ β§ ((π Β· π)(-gβπ
)(π Β· π)) β π΅ β§ (π Β· π) β π΅) β§ 0 β€ ((π Β· π)(-gβπ
)(π Β· π))) β ( 0 (+gβπ
)(π Β· π)) β€ (((π Β· π)(-gβπ
)(π Β· π))(+gβπ
)(π Β· π))) |
42 | 6, 14, 25, 22, 39, 41 | syl131anc 1380 |
. 2
β’ (π β ( 0 (+gβπ
)(π Β· π)) β€ (((π Β· π)(-gβπ
)(π Β· π))(+gβπ
)(π Β· π))) |
43 | 11, 40, 12 | grplid 18897 |
. . 3
β’ ((π
β Grp β§ (π Β· π) β π΅) β ( 0 (+gβπ
)(π Β· π)) = (π Β· π)) |
44 | 10, 22, 43 | syl2anc 583 |
. 2
β’ (π β ( 0 (+gβπ
)(π Β· π)) = (π Β· π)) |
45 | 11, 40, 23 | grpnpcan 18960 |
. . 3
β’ ((π
β Grp β§ (π Β· π) β π΅ β§ (π Β· π) β π΅) β (((π Β· π)(-gβπ
)(π Β· π))(+gβπ
)(π Β· π)) = (π Β· π)) |
46 | 10, 19, 22, 45 | syl3anc 1368 |
. 2
β’ (π β (((π Β· π)(-gβπ
)(π Β· π))(+gβπ
)(π Β· π)) = (π Β· π)) |
47 | 42, 44, 46 | 3brtr3d 5172 |
1
β’ (π β (π Β· π) β€ (π Β· π)) |