Step | Hyp | Ref
| Expression |
1 | | crngunit.1 |
. . . . 5
β’ π = (Unitβπ
) |
2 | 1 | a1i 9 |
. . . 4
β’ (π
β CRing β π = (Unitβπ
)) |
3 | | crngunit.2 |
. . . . 5
β’ 1 =
(1rβπ
) |
4 | 3 | a1i 9 |
. . . 4
β’ (π
β CRing β 1 =
(1rβπ
)) |
5 | | crngunit.3 |
. . . . 5
β’ β₯ =
(β₯rβπ
) |
6 | 5 | a1i 9 |
. . . 4
β’ (π
β CRing β β₯ =
(β₯rβπ
)) |
7 | | eqidd 2178 |
. . . 4
β’ (π
β CRing β
(opprβπ
) = (opprβπ
)) |
8 | | eqidd 2178 |
. . . 4
β’ (π
β CRing β
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
))) |
9 | | crngring 13191 |
. . . . 5
β’ (π
β CRing β π
β Ring) |
10 | | ringsrg 13224 |
. . . . 5
β’ (π
β Ring β π
β SRing) |
11 | 9, 10 | syl 14 |
. . . 4
β’ (π
β CRing β π
β SRing) |
12 | 2, 4, 6, 7, 8, 11 | isunitd 13275 |
. . 3
β’ (π
β CRing β (π β π β (π β₯ 1 β§ π(β₯rβ(opprβπ
)) 1 ))) |
13 | | eqid 2177 |
. . . . . . . . . . . 12
β’
(Baseβπ
) =
(Baseβπ
) |
14 | | eqid 2177 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (.rβπ
) |
15 | | eqid 2177 |
. . . . . . . . . . . 12
β’
(opprβπ
) = (opprβπ
) |
16 | | eqid 2177 |
. . . . . . . . . . . 12
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
17 | 13, 14, 15, 16 | crngoppr 13244 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π¦ β (Baseβπ
) β§ π β (Baseβπ
)) β (π¦(.rβπ
)π) = (π¦(.rβ(opprβπ
))π)) |
18 | 17 | 3expa 1203 |
. . . . . . . . . 10
β’ (((π
β CRing β§ π¦ β (Baseβπ
)) β§ π β (Baseβπ
)) β (π¦(.rβπ
)π) = (π¦(.rβ(opprβπ
))π)) |
19 | 18 | eqcomd 2183 |
. . . . . . . . 9
β’ (((π
β CRing β§ π¦ β (Baseβπ
)) β§ π β (Baseβπ
)) β (π¦(.rβ(opprβπ
))π) = (π¦(.rβπ
)π)) |
20 | 19 | an32s 568 |
. . . . . . . 8
β’ (((π
β CRing β§ π β (Baseβπ
)) β§ π¦ β (Baseβπ
)) β (π¦(.rβ(opprβπ
))π) = (π¦(.rβπ
)π)) |
21 | 20 | eqeq1d 2186 |
. . . . . . 7
β’ (((π
β CRing β§ π β (Baseβπ
)) β§ π¦ β (Baseβπ
)) β ((π¦(.rβ(opprβπ
))π) = 1 β (π¦(.rβπ
)π)
= 1
)) |
22 | 21 | rexbidva 2474 |
. . . . . 6
β’ ((π
β CRing β§ π β (Baseβπ
)) β (βπ¦ β (Baseβπ
)(π¦(.rβ(opprβπ
))π) = 1 β βπ¦ β (Baseβπ
)(π¦(.rβπ
)π)
= 1
)) |
23 | 22 | pm5.32da 452 |
. . . . 5
β’ (π
β CRing β ((π β (Baseβπ
) β§ βπ¦ β (Baseβπ
)(π¦(.rβ(opprβπ
))π) = 1 ) β (π β (Baseβπ
) β§ βπ¦ β (Baseβπ
)(π¦(.rβπ
)π)
= 1
))) |
24 | 15, 13 | opprbasg 13247 |
. . . . . 6
β’ (π
β CRing β
(Baseβπ
) =
(Baseβ(opprβπ
))) |
25 | 15 | opprring 13249 |
. . . . . . 7
β’ (π
β Ring β
(opprβπ
) β Ring) |
26 | | ringsrg 13224 |
. . . . . . 7
β’
((opprβπ
) β Ring β
(opprβπ
) β SRing) |
27 | 9, 25, 26 | 3syl 17 |
. . . . . 6
β’ (π
β CRing β
(opprβπ
) β SRing) |
28 | | eqidd 2178 |
. . . . . 6
β’ (π
β CRing β
(.rβ(opprβπ
)) =
(.rβ(opprβπ
))) |
29 | 24, 8, 27, 28 | dvdsrd 13263 |
. . . . 5
β’ (π
β CRing β (π(β₯rβ(opprβπ
)) 1 β (π β (Baseβπ
) β§ βπ¦ β (Baseβπ
)(π¦(.rβ(opprβπ
))π) = 1 ))) |
30 | | eqidd 2178 |
. . . . . 6
β’ (π
β CRing β
(Baseβπ
) =
(Baseβπ
)) |
31 | | eqidd 2178 |
. . . . . 6
β’ (π
β CRing β
(.rβπ
) =
(.rβπ
)) |
32 | 30, 6, 11, 31 | dvdsrd 13263 |
. . . . 5
β’ (π
β CRing β (π β₯ 1 β (π β (Baseβπ
) β§ βπ¦ β (Baseβπ
)(π¦(.rβπ
)π) = 1 ))) |
33 | 23, 29, 32 | 3bitr4d 220 |
. . . 4
β’ (π
β CRing β (π(β₯rβ(opprβπ
)) 1 β π β₯ 1 )) |
34 | 33 | anbi2d 464 |
. . 3
β’ (π
β CRing β ((π β₯ 1 β§ π(β₯rβ(opprβπ
)) 1 ) β (π β₯ 1 β§ π β₯ 1 ))) |
35 | 12, 34 | bitrd 188 |
. 2
β’ (π
β CRing β (π β π β (π β₯ 1 β§ π β₯ 1 ))) |
36 | | pm4.24 395 |
. 2
β’ (π β₯ 1 β (π β₯ 1 β§ π β₯ 1 )) |
37 | 35, 36 | bitr4di 198 |
1
β’ (π
β CRing β (π β π β π β₯ 1 )) |