Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β π
β Ring) |
2 | | simp3 1135 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β π β π) |
3 | | eqid 2726 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
4 | | unitmulcl.1 |
. . . . . . 7
β’ π = (Unitβπ
) |
5 | 3, 4 | unitcl 20277 |
. . . . . 6
β’ (π β π β π β (Baseβπ
)) |
6 | 2, 5 | syl 17 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β π β (Baseβπ
)) |
7 | | simp2 1134 |
. . . . . . 7
β’ ((π
β Ring β§ π β π β§ π β π) β π β π) |
8 | | eqid 2726 |
. . . . . . . 8
β’
(1rβπ
) = (1rβπ
) |
9 | | eqid 2726 |
. . . . . . . 8
β’
(β₯rβπ
) = (β₯rβπ
) |
10 | | eqid 2726 |
. . . . . . . 8
β’
(opprβπ
) = (opprβπ
) |
11 | | eqid 2726 |
. . . . . . . 8
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
12 | 4, 8, 9, 10, 11 | isunit 20275 |
. . . . . . 7
β’ (π β π β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
13 | 7, 12 | sylib 217 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
14 | 13 | simpld 494 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β π(β₯rβπ
)(1rβπ
)) |
15 | | unitmulcl.2 |
. . . . . 6
β’ Β· =
(.rβπ
) |
16 | 3, 9, 15 | dvdsrmul1 20271 |
. . . . 5
β’ ((π
β Ring β§ π β (Baseβπ
) β§ π(β₯rβπ
)(1rβπ
)) β (π Β· π)(β₯rβπ
)((1rβπ
) Β· π)) |
17 | 1, 6, 14, 16 | syl3anc 1368 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβπ
)((1rβπ
) Β· π)) |
18 | 3, 15, 8 | ringlidm 20168 |
. . . . 5
β’ ((π
β Ring β§ π β (Baseβπ
)) β
((1rβπ
)
Β·
π) = π) |
19 | 1, 6, 18 | syl2anc 583 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β ((1rβπ
) Β· π) = π) |
20 | 17, 19 | breqtrd 5167 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβπ
)π) |
21 | 4, 8, 9, 10, 11 | isunit 20275 |
. . . . 5
β’ (π β π β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
22 | 2, 21 | sylib 217 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
23 | 22 | simpld 494 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β π(β₯rβπ
)(1rβπ
)) |
24 | 3, 9 | dvdsrtr 20270 |
. . 3
β’ ((π
β Ring β§ (π Β· π)(β₯rβπ
)π β§ π(β₯rβπ
)(1rβπ
)) β (π Β· π)(β₯rβπ
)(1rβπ
)) |
25 | 1, 20, 23, 24 | syl3anc 1368 |
. 2
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβπ
)(1rβπ
)) |
26 | 10 | opprring 20249 |
. . . 4
β’ (π
β Ring β
(opprβπ
) β Ring) |
27 | 1, 26 | syl 17 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β (opprβπ
) β Ring) |
28 | | eqid 2726 |
. . . . 5
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
29 | 3, 15, 10, 28 | opprmul 20239 |
. . . 4
β’ (π(.rβ(opprβπ
))π) = (π Β· π) |
30 | 3, 4 | unitcl 20277 |
. . . . . . 7
β’ (π β π β π β (Baseβπ
)) |
31 | 7, 30 | syl 17 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β π β (Baseβπ
)) |
32 | 22 | simprd 495 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β π(β₯rβ(opprβπ
))(1rβπ
)) |
33 | 10, 3 | opprbas 20243 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβ(opprβπ
)) |
34 | 33, 11, 28 | dvdsrmul1 20271 |
. . . . . 6
β’
(((opprβπ
) β Ring β§ π β (Baseβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
)) β (π(.rβ(opprβπ
))π)(β₯rβ(opprβπ
))((1rβπ
)(.rβ(opprβπ
))π)) |
35 | 27, 31, 32, 34 | syl3anc 1368 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β (π(.rβ(opprβπ
))π)(β₯rβ(opprβπ
))((1rβπ
)(.rβ(opprβπ
))π)) |
36 | 3, 15, 10, 28 | opprmul 20239 |
. . . . . 6
β’
((1rβπ
)(.rβ(opprβπ
))π) = (π Β· (1rβπ
)) |
37 | 3, 15, 8 | ringridm 20169 |
. . . . . . 7
β’ ((π
β Ring β§ π β (Baseβπ
)) β (π Β·
(1rβπ
)) =
π) |
38 | 1, 31, 37 | syl2anc 583 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β·
(1rβπ
)) =
π) |
39 | 36, 38 | eqtrid 2778 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β ((1rβπ
)(.rβ(opprβπ
))π) = π) |
40 | 35, 39 | breqtrd 5167 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β (π(.rβ(opprβπ
))π)(β₯rβ(opprβπ
))π) |
41 | 29, 40 | eqbrtrrid 5177 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβ(opprβπ
))π) |
42 | 13 | simprd 495 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β π(β₯rβ(opprβπ
))(1rβπ
)) |
43 | 33, 11 | dvdsrtr 20270 |
. . 3
β’
(((opprβπ
) β Ring β§ (π Β· π)(β₯rβ(opprβπ
))π β§ π(β₯rβ(opprβπ
))(1rβπ
)) β (π Β· π)(β₯rβ(opprβπ
))(1rβπ
)) |
44 | 27, 41, 42, 43 | syl3anc 1368 |
. 2
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβ(opprβπ
))(1rβπ
)) |
45 | 4, 8, 9, 10, 11 | isunit 20275 |
. 2
β’ ((π Β· π) β π β ((π Β· π)(β₯rβπ
)(1rβπ
) β§ (π Β· π)(β₯rβ(opprβπ
))(1rβπ
))) |
46 | 25, 44, 45 | sylanbrc 582 |
1
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π) β π) |