Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((π
β Ring β§ π β π) β π
β Ring) |
2 | | ringgrp 19970 |
. . . . . 6
β’ (π
β Ring β π
β Grp) |
3 | | eqid 2737 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
4 | | unitnegcl.1 |
. . . . . . 7
β’ π = (Unitβπ
) |
5 | 3, 4 | unitcl 20089 |
. . . . . 6
β’ (π β π β π β (Baseβπ
)) |
6 | | unitnegcl.2 |
. . . . . . 7
β’ π = (invgβπ
) |
7 | 3, 6 | grpinvcl 18799 |
. . . . . 6
β’ ((π
β Grp β§ π β (Baseβπ
)) β (πβπ) β (Baseβπ
)) |
8 | 2, 5, 7 | syl2an 597 |
. . . . 5
β’ ((π
β Ring β§ π β π) β (πβπ) β (Baseβπ
)) |
9 | | eqid 2737 |
. . . . . 6
β’
(β₯rβπ
) = (β₯rβπ
) |
10 | 3, 9, 6 | dvdsrneg 20084 |
. . . . 5
β’ ((π
β Ring β§ (πβπ) β (Baseβπ
)) β (πβπ)(β₯rβπ
)(πβ(πβπ))) |
11 | 8, 10 | syldan 592 |
. . . 4
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβπ
)(πβ(πβπ))) |
12 | 3, 6 | grpinvinv 18815 |
. . . . 5
β’ ((π
β Grp β§ π β (Baseβπ
)) β (πβ(πβπ)) = π) |
13 | 2, 5, 12 | syl2an 597 |
. . . 4
β’ ((π
β Ring β§ π β π) β (πβ(πβπ)) = π) |
14 | 11, 13 | breqtrd 5132 |
. . 3
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβπ
)π) |
15 | | simpr 486 |
. . . . 5
β’ ((π
β Ring β§ π β π) β π β π) |
16 | | eqid 2737 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
17 | | eqid 2737 |
. . . . . 6
β’
(opprβπ
) = (opprβπ
) |
18 | | eqid 2737 |
. . . . . 6
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
19 | 4, 16, 9, 17, 18 | isunit 20087 |
. . . . 5
β’ (π β π β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
20 | 15, 19 | sylib 217 |
. . . 4
β’ ((π
β Ring β§ π β π) β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
21 | 20 | simpld 496 |
. . 3
β’ ((π
β Ring β§ π β π) β π(β₯rβπ
)(1rβπ
)) |
22 | 3, 9 | dvdsrtr 20082 |
. . 3
β’ ((π
β Ring β§ (πβπ)(β₯rβπ
)π β§ π(β₯rβπ
)(1rβπ
)) β (πβπ)(β₯rβπ
)(1rβπ
)) |
23 | 1, 14, 21, 22 | syl3anc 1372 |
. 2
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβπ
)(1rβπ
)) |
24 | 17 | opprring 20061 |
. . . 4
β’ (π
β Ring β
(opprβπ
) β Ring) |
25 | 24 | adantr 482 |
. . 3
β’ ((π
β Ring β§ π β π) β (opprβπ
) β Ring) |
26 | 17, 3 | opprbas 20057 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβ(opprβπ
)) |
27 | 17, 6 | opprneg 20065 |
. . . . . 6
β’ π =
(invgβ(opprβπ
)) |
28 | 26, 18, 27 | dvdsrneg 20084 |
. . . . 5
β’
(((opprβπ
) β Ring β§ (πβπ) β (Baseβπ
)) β (πβπ)(β₯rβ(opprβπ
))(πβ(πβπ))) |
29 | 25, 8, 28 | syl2anc 585 |
. . . 4
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβ(opprβπ
))(πβ(πβπ))) |
30 | 29, 13 | breqtrd 5132 |
. . 3
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβ(opprβπ
))π) |
31 | 20 | simprd 497 |
. . 3
β’ ((π
β Ring β§ π β π) β π(β₯rβ(opprβπ
))(1rβπ
)) |
32 | 26, 18 | dvdsrtr 20082 |
. . 3
β’
(((opprβπ
) β Ring β§ (πβπ)(β₯rβ(opprβπ
))π β§ π(β₯rβ(opprβπ
))(1rβπ
)) β (πβπ)(β₯rβ(opprβπ
))(1rβπ
)) |
33 | 25, 30, 31, 32 | syl3anc 1372 |
. 2
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβ(opprβπ
))(1rβπ
)) |
34 | 4, 16, 9, 17, 18 | isunit 20087 |
. 2
β’ ((πβπ) β π β ((πβπ)(β₯rβπ
)(1rβπ
) β§ (πβπ)(β₯rβ(opprβπ
))(1rβπ
))) |
35 | 23, 33, 34 | sylanbrc 584 |
1
β’ ((π
β Ring β§ π β π) β (πβπ) β π) |