Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β π
β Ring) |
2 | | eqidd 2178 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β (Baseβπ
) = (Baseβπ
)) |
3 | | unitmulcl.1 |
. . . . . . 7
β’ π = (Unitβπ
) |
4 | 3 | a1i 9 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β π = (Unitβπ
)) |
5 | | ringsrg 13224 |
. . . . . . 7
β’ (π
β Ring β π
β SRing) |
6 | 1, 5 | syl 14 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β π
β SRing) |
7 | | simp3 999 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β π β π) |
8 | 2, 4, 6, 7 | unitcld 13277 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β π β (Baseβπ
)) |
9 | | simp2 998 |
. . . . . . 7
β’ ((π
β Ring β§ π β π β§ π β π) β π β π) |
10 | | eqidd 2178 |
. . . . . . . 8
β’ ((π
β Ring β§ π β π β§ π β π) β (1rβπ
) = (1rβπ
)) |
11 | | eqidd 2178 |
. . . . . . . 8
β’ ((π
β Ring β§ π β π β§ π β π) β (β₯rβπ
) =
(β₯rβπ
)) |
12 | | eqidd 2178 |
. . . . . . . 8
β’ ((π
β Ring β§ π β π β§ π β π) β (opprβπ
) =
(opprβπ
)) |
13 | | eqidd 2178 |
. . . . . . . 8
β’ ((π
β Ring β§ π β π β§ π β π) β
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
))) |
14 | 4, 10, 11, 12, 13, 6 | isunitd 13275 |
. . . . . . 7
β’ ((π
β Ring β§ π β π β§ π β π) β (π β π β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
)))) |
15 | 9, 14 | mpbid 147 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
16 | 15 | simpld 112 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β π(β₯rβπ
)(1rβπ
)) |
17 | | eqid 2177 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
18 | | eqid 2177 |
. . . . . 6
β’
(β₯rβπ
) = (β₯rβπ
) |
19 | | unitmulcl.2 |
. . . . . 6
β’ Β· =
(.rβπ
) |
20 | 17, 18, 19 | dvdsrmul1 13271 |
. . . . 5
β’ ((π
β Ring β§ π β (Baseβπ
) β§ π(β₯rβπ
)(1rβπ
)) β (π Β· π)(β₯rβπ
)((1rβπ
) Β· π)) |
21 | 1, 8, 16, 20 | syl3anc 1238 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβπ
)((1rβπ
) Β· π)) |
22 | | eqid 2177 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
23 | 17, 19, 22 | ringlidm 13206 |
. . . . 5
β’ ((π
β Ring β§ π β (Baseβπ
)) β
((1rβπ
)
Β·
π) = π) |
24 | 1, 8, 23 | syl2anc 411 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β ((1rβπ
) Β· π) = π) |
25 | 21, 24 | breqtrd 4030 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβπ
)π) |
26 | 4, 10, 11, 12, 13, 6 | isunitd 13275 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β (π β π β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
)))) |
27 | 7, 26 | mpbid 147 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β (π(β₯rβπ
)(1rβπ
) β§ π(β₯rβ(opprβπ
))(1rβπ
))) |
28 | 27 | simpld 112 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β π(β₯rβπ
)(1rβπ
)) |
29 | 17, 18 | dvdsrtr 13270 |
. . 3
β’ ((π
β Ring β§ (π Β· π)(β₯rβπ
)π β§ π(β₯rβπ
)(1rβπ
)) β (π Β· π)(β₯rβπ
)(1rβπ
)) |
30 | 1, 25, 28, 29 | syl3anc 1238 |
. 2
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβπ
)(1rβπ
)) |
31 | | eqid 2177 |
. . . . 5
β’
(opprβπ
) = (opprβπ
) |
32 | 31 | opprring 13249 |
. . . 4
β’ (π
β Ring β
(opprβπ
) β Ring) |
33 | 1, 32 | syl 14 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β (opprβπ
) β Ring) |
34 | 2, 4, 6, 9 | unitcld 13277 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β π β (Baseβπ
)) |
35 | 31, 17 | opprbasg 13247 |
. . . . . . 7
β’ (π
β Ring β
(Baseβπ
) =
(Baseβ(opprβπ
))) |
36 | 1, 35 | syl 14 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β (Baseβπ
) =
(Baseβ(opprβπ
))) |
37 | 34, 36 | eleqtrd 2256 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β π β
(Baseβ(opprβπ
))) |
38 | 27 | simprd 114 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β π(β₯rβ(opprβπ
))(1rβπ
)) |
39 | | eqid 2177 |
. . . . . 6
β’
(Baseβ(opprβπ
)) =
(Baseβ(opprβπ
)) |
40 | | eqid 2177 |
. . . . . 6
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
41 | | eqid 2177 |
. . . . . 6
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
42 | 39, 40, 41 | dvdsrmul1 13271 |
. . . . 5
β’
(((opprβπ
) β Ring β§ π β
(Baseβ(opprβπ
)) β§ π(β₯rβ(opprβπ
))(1rβπ
)) β (π(.rβ(opprβπ
))π)(β₯rβ(opprβπ
))((1rβπ
)(.rβ(opprβπ
))π)) |
43 | 33, 37, 38, 42 | syl3anc 1238 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β (π(.rβ(opprβπ
))π)(β₯rβ(opprβπ
))((1rβπ
)(.rβ(opprβπ
))π)) |
44 | 17, 19, 31, 41 | opprmulg 13243 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β (π(.rβ(opprβπ
))π) = (π Β· π)) |
45 | 44 | 3com23 1209 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β (π(.rβ(opprβπ
))π) = (π Β· π)) |
46 | 17, 22 | srgidcl 13159 |
. . . . . . 7
β’ (π
β SRing β
(1rβπ
)
β (Baseβπ
)) |
47 | 6, 46 | syl 14 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β (1rβπ
) β (Baseβπ
)) |
48 | 17, 19, 31, 41 | opprmulg 13243 |
. . . . . 6
β’ ((π
β Ring β§
(1rβπ
)
β (Baseβπ
) β§
π β π) β ((1rβπ
)(.rβ(opprβπ
))π) = (π Β· (1rβπ
))) |
49 | 1, 47, 9, 48 | syl3anc 1238 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β ((1rβπ
)(.rβ(opprβπ
))π) = (π Β· (1rβπ
))) |
50 | 17, 19, 22 | ringridm 13207 |
. . . . . 6
β’ ((π
β Ring β§ π β (Baseβπ
)) β (π Β·
(1rβπ
)) =
π) |
51 | 1, 34, 50 | syl2anc 411 |
. . . . 5
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β·
(1rβπ
)) =
π) |
52 | 49, 51 | eqtrd 2210 |
. . . 4
β’ ((π
β Ring β§ π β π β§ π β π) β ((1rβπ
)(.rβ(opprβπ
))π) = π) |
53 | 43, 45, 52 | 3brtr3d 4035 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβ(opprβπ
))π) |
54 | 15 | simprd 114 |
. . 3
β’ ((π
β Ring β§ π β π β§ π β π) β π(β₯rβ(opprβπ
))(1rβπ
)) |
55 | 39, 40 | dvdsrtr 13270 |
. . 3
β’
(((opprβπ
) β Ring β§ (π Β· π)(β₯rβ(opprβπ
))π β§ π(β₯rβ(opprβπ
))(1rβπ
)) β (π Β· π)(β₯rβ(opprβπ
))(1rβπ
)) |
56 | 33, 53, 54, 55 | syl3anc 1238 |
. 2
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π)(β₯rβ(opprβπ
))(1rβπ
)) |
57 | 4, 10, 11, 12, 13, 6 | isunitd 13275 |
. 2
β’ ((π
β Ring β§ π β π β§ π β π) β ((π Β· π) β π β ((π Β· π)(β₯rβπ
)(1rβπ
) β§ (π Β· π)(β₯rβ(opprβπ
))(1rβπ
)))) |
58 | 30, 56, 57 | mpbir2and 944 |
1
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π) β π) |