Step | Hyp | Ref
| Expression |
1 | | opprunitd.1 |
. . . . . 6
β’ (π β π = (Unitβπ
)) |
2 | | eqidd 2178 |
. . . . . 6
β’ (π β (1rβπ
) = (1rβπ
)) |
3 | | eqidd 2178 |
. . . . . 6
β’ (π β
(β₯rβπ
) = (β₯rβπ
)) |
4 | | opprunitd.2 |
. . . . . 6
β’ (π β π = (opprβπ
)) |
5 | | eqidd 2178 |
. . . . . 6
β’ (π β
(β₯rβπ) = (β₯rβπ)) |
6 | | opprunitd.r |
. . . . . . 7
β’ (π β π
β Ring) |
7 | | ringsrg 13222 |
. . . . . . 7
β’ (π
β Ring β π
β SRing) |
8 | 6, 7 | syl 14 |
. . . . . 6
β’ (π β π
β SRing) |
9 | 1, 2, 3, 4, 5, 8 | isunitd 13273 |
. . . . 5
β’ (π β (π₯ β π β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβπ)(1rβπ
)))) |
10 | | eqid 2177 |
. . . . . . . . . . . . . . 15
β’
(opprβπ
) = (opprβπ
) |
11 | 10 | opprring 13247 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β
(opprβπ
) β Ring) |
12 | 6, 11 | syl 14 |
. . . . . . . . . . . . 13
β’ (π β
(opprβπ
) β Ring) |
13 | 4, 12 | eqeltrd 2254 |
. . . . . . . . . . . 12
β’ (π β π β Ring) |
14 | | vex 2740 |
. . . . . . . . . . . . 13
β’ π¦ β V |
15 | 14 | a1i 9 |
. . . . . . . . . . . 12
β’ (π β π¦ β V) |
16 | | vex 2740 |
. . . . . . . . . . . . 13
β’ π₯ β V |
17 | 16 | a1i 9 |
. . . . . . . . . . . 12
β’ (π β π₯ β V) |
18 | | eqid 2177 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
19 | | eqid 2177 |
. . . . . . . . . . . . 13
β’
(.rβπ) = (.rβπ) |
20 | | eqid 2177 |
. . . . . . . . . . . . 13
β’
(opprβπ) = (opprβπ) |
21 | | eqid 2177 |
. . . . . . . . . . . . 13
β’
(.rβ(opprβπ)) =
(.rβ(opprβπ)) |
22 | 18, 19, 20, 21 | opprmulg 13241 |
. . . . . . . . . . . 12
β’ ((π β Ring β§ π¦ β V β§ π₯ β V) β (π¦(.rβ(opprβπ))π₯) = (π₯(.rβπ)π¦)) |
23 | 13, 15, 17, 22 | syl3anc 1238 |
. . . . . . . . . . 11
β’ (π β (π¦(.rβ(opprβπ))π₯) = (π₯(.rβπ)π¦)) |
24 | 4 | fveq2d 5519 |
. . . . . . . . . . . 12
β’ (π β (.rβπ) =
(.rβ(opprβπ
))) |
25 | 24 | oveqd 5891 |
. . . . . . . . . . 11
β’ (π β (π₯(.rβπ)π¦) = (π₯(.rβ(opprβπ
))π¦)) |
26 | | eqid 2177 |
. . . . . . . . . . . . 13
β’
(Baseβπ
) =
(Baseβπ
) |
27 | | eqid 2177 |
. . . . . . . . . . . . 13
β’
(.rβπ
) = (.rβπ
) |
28 | | eqid 2177 |
. . . . . . . . . . . . 13
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
29 | 26, 27, 10, 28 | opprmulg 13241 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π₯ β V β§ π¦ β V) β (π₯(.rβ(opprβπ
))π¦) = (π¦(.rβπ
)π₯)) |
30 | 6, 17, 15, 29 | syl3anc 1238 |
. . . . . . . . . . 11
β’ (π β (π₯(.rβ(opprβπ
))π¦) = (π¦(.rβπ
)π₯)) |
31 | 23, 25, 30 | 3eqtrrd 2215 |
. . . . . . . . . 10
β’ (π β (π¦(.rβπ
)π₯) = (π¦(.rβ(opprβπ))π₯)) |
32 | 31 | eqeq1d 2186 |
. . . . . . . . 9
β’ (π β ((π¦(.rβπ
)π₯) = (1rβπ
) β (π¦(.rβ(opprβπ))π₯) = (1rβπ
))) |
33 | 32 | rexbidv 2478 |
. . . . . . . 8
β’ (π β (βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
) β βπ¦ β (Baseβπ
)(π¦(.rβ(opprβπ))π₯) = (1rβπ
))) |
34 | 33 | anbi2d 464 |
. . . . . . 7
β’ (π β ((π₯ β (Baseβπ
) β§ βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
)) β (π₯ β (Baseβπ
) β§ βπ¦ β (Baseβπ
)(π¦(.rβ(opprβπ))π₯) = (1rβπ
)))) |
35 | | eqidd 2178 |
. . . . . . . 8
β’ (π β (Baseβπ
) = (Baseβπ
)) |
36 | | eqidd 2178 |
. . . . . . . 8
β’ (π β (.rβπ
) = (.rβπ
)) |
37 | 35, 3, 8, 36 | dvdsrd 13261 |
. . . . . . 7
β’ (π β (π₯(β₯rβπ
)(1rβπ
) β (π₯ β (Baseβπ
) β§ βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
)))) |
38 | 10, 26 | opprbasg 13245 |
. . . . . . . . . 10
β’ (π
β SRing β
(Baseβπ
) =
(Baseβ(opprβπ
))) |
39 | 8, 38 | syl 14 |
. . . . . . . . 9
β’ (π β (Baseβπ
) =
(Baseβ(opprβπ
))) |
40 | 4 | fveq2d 5519 |
. . . . . . . . 9
β’ (π β (Baseβπ) =
(Baseβ(opprβπ
))) |
41 | 20, 18 | opprbasg 13245 |
. . . . . . . . . 10
β’ (π β Ring β
(Baseβπ) =
(Baseβ(opprβπ))) |
42 | 13, 41 | syl 14 |
. . . . . . . . 9
β’ (π β (Baseβπ) =
(Baseβ(opprβπ))) |
43 | 39, 40, 42 | 3eqtr2d 2216 |
. . . . . . . 8
β’ (π β (Baseβπ
) =
(Baseβ(opprβπ))) |
44 | | eqidd 2178 |
. . . . . . . 8
β’ (π β
(β₯rβ(opprβπ)) =
(β₯rβ(opprβπ))) |
45 | 20 | opprring 13247 |
. . . . . . . . . 10
β’ (π β Ring β
(opprβπ) β Ring) |
46 | 13, 45 | syl 14 |
. . . . . . . . 9
β’ (π β
(opprβπ) β Ring) |
47 | | ringsrg 13222 |
. . . . . . . . 9
β’
((opprβπ) β Ring β
(opprβπ) β SRing) |
48 | 46, 47 | syl 14 |
. . . . . . . 8
β’ (π β
(opprβπ) β SRing) |
49 | | eqidd 2178 |
. . . . . . . 8
β’ (π β
(.rβ(opprβπ)) =
(.rβ(opprβπ))) |
50 | 43, 44, 48, 49 | dvdsrd 13261 |
. . . . . . 7
β’ (π β (π₯(β₯rβ(opprβπ))(1rβπ
) β (π₯ β (Baseβπ
) β§ βπ¦ β (Baseβπ
)(π¦(.rβ(opprβπ))π₯) = (1rβπ
)))) |
51 | 34, 37, 50 | 3bitr4d 220 |
. . . . . 6
β’ (π β (π₯(β₯rβπ
)(1rβπ
) β π₯(β₯rβ(opprβπ))(1rβπ
))) |
52 | 51 | anbi1d 465 |
. . . . 5
β’ (π β ((π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβπ)(1rβπ
)) β (π₯(β₯rβ(opprβπ))(1rβπ
) β§ π₯(β₯rβπ)(1rβπ
)))) |
53 | 9, 52 | bitrd 188 |
. . . 4
β’ (π β (π₯ β π β (π₯(β₯rβ(opprβπ))(1rβπ
) β§ π₯(β₯rβπ)(1rβπ
)))) |
54 | 53 | biancomd 271 |
. . 3
β’ (π β (π₯ β π β (π₯(β₯rβπ)(1rβπ
) β§ π₯(β₯rβ(opprβπ))(1rβπ
)))) |
55 | | eqidd 2178 |
. . . 4
β’ (π β (Unitβπ) = (Unitβπ)) |
56 | | eqid 2177 |
. . . . . . 7
β’
(1rβπ
) = (1rβπ
) |
57 | 10, 56 | oppr1g 13250 |
. . . . . 6
β’ (π
β Ring β
(1rβπ
) =
(1rβ(opprβπ
))) |
58 | 6, 57 | syl 14 |
. . . . 5
β’ (π β (1rβπ
) =
(1rβ(opprβπ
))) |
59 | 4 | fveq2d 5519 |
. . . . 5
β’ (π β (1rβπ) =
(1rβ(opprβπ
))) |
60 | 58, 59 | eqtr4d 2213 |
. . . 4
β’ (π β (1rβπ
) = (1rβπ)) |
61 | | eqidd 2178 |
. . . 4
β’ (π β
(opprβπ) = (opprβπ)) |
62 | | ringsrg 13222 |
. . . . 5
β’ (π β Ring β π β SRing) |
63 | 13, 62 | syl 14 |
. . . 4
β’ (π β π β SRing) |
64 | 55, 60, 5, 61, 44, 63 | isunitd 13273 |
. . 3
β’ (π β (π₯ β (Unitβπ) β (π₯(β₯rβπ)(1rβπ
) β§ π₯(β₯rβ(opprβπ))(1rβπ
)))) |
65 | 54, 64 | bitr4d 191 |
. 2
β’ (π β (π₯ β π β π₯ β (Unitβπ))) |
66 | 65 | eqrdv 2175 |
1
β’ (π β π = (Unitβπ)) |