Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . 3
β’ ((π
β Ring β§ π β π) β π
β Ring) |
2 | | ringgrp 13189 |
. . . . . 6
β’ (π
β Ring β π
β Grp) |
3 | | eqidd 2178 |
. . . . . . 7
β’ ((π
β Ring β§ π β π) β (Baseβπ
) = (Baseβπ
)) |
4 | | unitnegcl.1 |
. . . . . . . 8
β’ π = (Unitβπ
) |
5 | 4 | a1i 9 |
. . . . . . 7
β’ ((π
β Ring β§ π β π) β π = (Unitβπ
)) |
6 | | ringsrg 13229 |
. . . . . . . 8
β’ (π
β Ring β π
β SRing) |
7 | 6 | adantr 276 |
. . . . . . 7
β’ ((π
β Ring β§ π β π) β π
β SRing) |
8 | | simpr 110 |
. . . . . . 7
β’ ((π
β Ring β§ π β π) β π β π) |
9 | 3, 5, 7, 8 | unitcld 13282 |
. . . . . 6
β’ ((π
β Ring β§ π β π) β π β (Baseβπ
)) |
10 | | eqid 2177 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
11 | | unitnegcl.2 |
. . . . . . 7
β’ π = (invgβπ
) |
12 | 10, 11 | grpinvcl 12926 |
. . . . . 6
β’ ((π
β Grp β§ π β (Baseβπ
)) β (πβπ) β (Baseβπ
)) |
13 | 2, 9, 12 | syl2an2r 595 |
. . . . 5
β’ ((π
β Ring β§ π β π) β (πβπ) β (Baseβπ
)) |
14 | | eqid 2177 |
. . . . . 6
β’
(β₯rβπ
) = (β₯rβπ
) |
15 | 10, 14, 11 | dvdsrneg 13277 |
. . . . 5
β’ ((π
β Ring β§ (πβπ) β (Baseβπ
)) β (πβπ)(β₯rβπ
)(πβ(πβπ))) |
16 | 13, 15 | syldan 282 |
. . . 4
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβπ
)(πβ(πβπ))) |
17 | 10, 11 | grpinvinv 12942 |
. . . . 5
β’ ((π
β Grp β§ π β (Baseβπ
)) β (πβ(πβπ)) = π) |
18 | 2, 9, 17 | syl2an2r 595 |
. . . 4
β’ ((π
β Ring β§ π β π) β (πβ(πβπ)) = π) |
19 | 16, 18 | breqtrd 4031 |
. . 3
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβπ
)π) |
20 | | eqidd 2178 |
. . . . . 6
β’ ((π
β Ring β§ π β π) β (1rβπ
) = (1rβπ
)) |
21 | | eqidd 2178 |
. . . . . 6
β’ ((π
β Ring β§ π β π) β (β₯rβπ
) =
(β₯rβπ
)) |
22 | | eqidd 2178 |
. . . . . 6
β’ ((π
β Ring β§ π β π) β (opprβπ
) =
(opprβπ
)) |
23 | | eqidd 2178 |
. . . . . 6
β’ ((π
β Ring β§ π β π) β
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
))) |
24 | 5, 20, 21, 22, 23, 7 | isunitd 13280 |
. . . . 5
β’ ((π
β Ring β§ π β π) β (π β π β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
)))) |
25 | 8, 24 | mpbid 147 |
. . . 4
β’ ((π
β Ring β§ π β π) β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
26 | 25 | simpld 112 |
. . 3
β’ ((π
β Ring β§ π β π) β π(β₯rβπ
)(1rβπ
)) |
27 | 10, 14 | dvdsrtr 13275 |
. . 3
β’ ((π
β Ring β§ (πβπ)(β₯rβπ
)π β§ π(β₯rβπ
)(1rβπ
)) β (πβπ)(β₯rβπ
)(1rβπ
)) |
28 | 1, 19, 26, 27 | syl3anc 1238 |
. 2
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβπ
)(1rβπ
)) |
29 | | eqid 2177 |
. . . . 5
β’
(opprβπ
) = (opprβπ
) |
30 | 29 | opprring 13254 |
. . . 4
β’ (π
β Ring β
(opprβπ
) β Ring) |
31 | 30 | adantr 276 |
. . 3
β’ ((π
β Ring β§ π β π) β (opprβπ
) β Ring) |
32 | 29, 10 | opprbasg 13252 |
. . . . . . . . 9
β’ (π
β Ring β
(Baseβπ
) =
(Baseβ(opprβπ
))) |
33 | 32 | eleq2d 2247 |
. . . . . . . 8
β’ (π
β Ring β ((πβπ) β (Baseβπ
) β (πβπ) β
(Baseβ(opprβπ
)))) |
34 | 33 | adantr 276 |
. . . . . . 7
β’ ((π
β Ring β§ π β π) β ((πβπ) β (Baseβπ
) β (πβπ) β
(Baseβ(opprβπ
)))) |
35 | 13, 34 | mpbid 147 |
. . . . . 6
β’ ((π
β Ring β§ π β π) β (πβπ) β
(Baseβ(opprβπ
))) |
36 | | eqid 2177 |
. . . . . . 7
β’
(Baseβ(opprβπ
)) =
(Baseβ(opprβπ
)) |
37 | | eqid 2177 |
. . . . . . 7
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
38 | | eqid 2177 |
. . . . . . 7
β’
(invgβ(opprβπ
)) =
(invgβ(opprβπ
)) |
39 | 36, 37, 38 | dvdsrneg 13277 |
. . . . . 6
β’
(((opprβπ
) β Ring β§ (πβπ) β
(Baseβ(opprβπ
))) β (πβπ)(β₯rβ(opprβπ
))((invgβ(opprβπ
))β(πβπ))) |
40 | 30, 35, 39 | syl2an2r 595 |
. . . . 5
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβ(opprβπ
))((invgβ(opprβπ
))β(πβπ))) |
41 | 29, 11 | opprnegg 13258 |
. . . . . . . 8
β’ (π
β Ring β π =
(invgβ(opprβπ
))) |
42 | 41 | fveq1d 5519 |
. . . . . . 7
β’ (π
β Ring β (πβ(πβπ)) =
((invgβ(opprβπ
))β(πβπ))) |
43 | 42 | breq2d 4017 |
. . . . . 6
β’ (π
β Ring β ((πβπ)(β₯rβ(opprβπ
))(πβ(πβπ))
β (πβπ)(β₯rβ(opprβπ
))((invgβ(opprβπ
))β(πβπ)))) |
44 | 43 | adantr 276 |
. . . . 5
β’ ((π
β Ring β§ π β π) β ((πβπ)(β₯rβ(opprβπ
))(πβ(πβπ))
β (πβπ)(β₯rβ(opprβπ
))((invgβ(opprβπ
))β(πβπ)))) |
45 | 40, 44 | mpbird 167 |
. . . 4
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβ(opprβπ
))(πβ(πβπ))) |
46 | 45, 18 | breqtrd 4031 |
. . 3
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβ(opprβπ
))π) |
47 | 25 | simprd 114 |
. . 3
β’ ((π
β Ring β§ π β π) β π(β₯rβ(opprβπ
))(1rβπ
)) |
48 | 36, 37 | dvdsrtr 13275 |
. . 3
β’
(((opprβπ
) β Ring β§ (πβπ)(β₯rβ(opprβπ
))π β§ π(β₯rβ(opprβπ
))(1rβπ
)) β (πβπ)(β₯rβ(opprβπ
))(1rβπ
)) |
49 | 31, 46, 47, 48 | syl3anc 1238 |
. 2
β’ ((π
β Ring β§ π β π) β (πβπ)(β₯rβ(opprβπ
))(1rβπ
)) |
50 | 5, 20, 21, 22, 23, 7 | isunitd 13280 |
. 2
β’ ((π
β Ring β§ π β π) β ((πβπ) β π β ((πβπ)(β₯rβπ
)(1rβπ
) β§ (πβπ)(β₯rβ(opprβπ
))(1rβπ
)))) |
51 | 28, 49, 50 | mpbir2and 944 |
1
β’ ((π
β Ring β§ π β π) β (πβπ) β π) |