Step | Hyp | Ref
| Expression |
1 | | unitgrp.1 |
. . . 4
β’ π = (Unitβπ
) |
2 | 1 | a1i 9 |
. . 3
β’ (π
β Ring β π = (Unitβπ
)) |
3 | | unitgrp.2 |
. . . 4
β’ πΊ = ((mulGrpβπ
) βΎs π) |
4 | 3 | a1i 9 |
. . 3
β’ (π
β Ring β πΊ = ((mulGrpβπ
) βΎs π)) |
5 | | ringsrg 13222 |
. . 3
β’ (π
β Ring β π
β SRing) |
6 | 2, 4, 5 | unitgrpbasd 13282 |
. 2
β’ (π
β Ring β π = (BaseβπΊ)) |
7 | | eqid 2177 |
. . . 4
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
8 | | eqid 2177 |
. . . 4
β’
(.rβπ
) = (.rβπ
) |
9 | 7, 8 | mgpplusgg 13132 |
. . 3
β’ (π
β Ring β
(.rβπ
) =
(+gβ(mulGrpβπ
))) |
10 | | basfn 12519 |
. . . . 5
β’ Base Fn
V |
11 | | elex 2748 |
. . . . 5
β’ (π
β Ring β π
β V) |
12 | | funfvex 5532 |
. . . . . 6
β’ ((Fun
Base β§ π
β dom
Base) β (Baseβπ
)
β V) |
13 | 12 | funfni 5316 |
. . . . 5
β’ ((Base Fn
V β§ π
β V) β
(Baseβπ
) β
V) |
14 | 10, 11, 13 | sylancr 414 |
. . . 4
β’ (π
β Ring β
(Baseβπ
) β
V) |
15 | | eqidd 2178 |
. . . . 5
β’ (π
β Ring β
(Baseβπ
) =
(Baseβπ
)) |
16 | 15, 2, 5 | unitssd 13276 |
. . . 4
β’ (π
β Ring β π β (Baseβπ
)) |
17 | 14, 16 | ssexd 4143 |
. . 3
β’ (π
β Ring β π β V) |
18 | 7 | mgpex 13133 |
. . 3
β’ (π
β Ring β
(mulGrpβπ
) β
V) |
19 | 4, 9, 17, 18 | ressplusgd 12586 |
. 2
β’ (π
β Ring β
(.rβπ
) =
(+gβπΊ)) |
20 | 1, 8 | unitmulcl 13280 |
. 2
β’ ((π
β Ring β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
21 | | eqidd 2178 |
. . . . 5
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (Baseβπ
) = (Baseβπ
)) |
22 | 1 | a1i 9 |
. . . . 5
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π = (Unitβπ
)) |
23 | 5 | adantr 276 |
. . . . 5
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π
β SRing) |
24 | | simpr1 1003 |
. . . . 5
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π₯ β π) |
25 | 21, 22, 23, 24 | unitcld 13275 |
. . . 4
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π₯ β (Baseβπ
)) |
26 | | simpr2 1004 |
. . . . 5
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π¦ β π) |
27 | 21, 22, 23, 26 | unitcld 13275 |
. . . 4
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π¦ β (Baseβπ
)) |
28 | | simpr3 1005 |
. . . . 5
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π§ β π) |
29 | 21, 22, 23, 28 | unitcld 13275 |
. . . 4
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π§ β (Baseβπ
)) |
30 | 25, 27, 29 | 3jca 1177 |
. . 3
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) |
31 | | eqid 2177 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
32 | 31, 8 | ringass 13197 |
. . 3
β’ ((π
β Ring β§ (π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) β ((π₯(.rβπ
)π¦)(.rβπ
)π§) = (π₯(.rβπ
)(π¦(.rβπ
)π§))) |
33 | 30, 32 | syldan 282 |
. 2
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯(.rβπ
)π¦)(.rβπ
)π§) = (π₯(.rβπ
)(π¦(.rβπ
)π§))) |
34 | | eqid 2177 |
. . 3
β’
(1rβπ
) = (1rβπ
) |
35 | 1, 34 | 1unit 13274 |
. 2
β’ (π
β Ring β
(1rβπ
)
β π) |
36 | | eqidd 2178 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β (Baseβπ
) = (Baseβπ
)) |
37 | 1 | a1i 9 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β π = (Unitβπ
)) |
38 | 5 | adantr 276 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β π
β SRing) |
39 | | simpr 110 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β π₯ β π) |
40 | 36, 37, 38, 39 | unitcld 13275 |
. . 3
β’ ((π
β Ring β§ π₯ β π) β π₯ β (Baseβπ
)) |
41 | 31, 8, 34 | ringlidm 13204 |
. . 3
β’ ((π
β Ring β§ π₯ β (Baseβπ
)) β
((1rβπ
)(.rβπ
)π₯) = π₯) |
42 | 40, 41 | syldan 282 |
. 2
β’ ((π
β Ring β§ π₯ β π) β ((1rβπ
)(.rβπ
)π₯) = π₯) |
43 | | eqidd 2178 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (1rβπ
) = (1rβπ
)) |
44 | | eqidd 2178 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (β₯rβπ
) =
(β₯rβπ
)) |
45 | | eqidd 2178 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (opprβπ
) =
(opprβπ
)) |
46 | | eqidd 2178 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
))) |
47 | 37, 43, 44, 45, 46, 38 | isunitd 13273 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β (π₯ β π β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
)))) |
48 | 39, 47 | mpbid 147 |
. . 3
β’ ((π
β Ring β§ π₯ β π) β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
))) |
49 | | eqidd 2178 |
. . . . . 6
β’ ((π
β Ring β§ π₯ β π) β (.rβπ
) = (.rβπ
)) |
50 | 36, 44, 38, 49, 40 | dvdsr2d 13262 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (π₯(β₯rβπ
)(1rβπ
) β βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
))) |
51 | | eqid 2177 |
. . . . . . . 8
β’
(opprβπ
) = (opprβπ
) |
52 | 51, 31 | opprbasg 13245 |
. . . . . . 7
β’ (π
β Ring β
(Baseβπ
) =
(Baseβ(opprβπ
))) |
53 | 52 | adantr 276 |
. . . . . 6
β’ ((π
β Ring β§ π₯ β π) β (Baseβπ
) =
(Baseβ(opprβπ
))) |
54 | 51 | opprring 13247 |
. . . . . . . 8
β’ (π
β Ring β
(opprβπ
) β Ring) |
55 | | ringsrg 13222 |
. . . . . . . 8
β’
((opprβπ
) β Ring β
(opprβπ
) β SRing) |
56 | 54, 55 | syl 14 |
. . . . . . 7
β’ (π
β Ring β
(opprβπ
) β SRing) |
57 | 56 | adantr 276 |
. . . . . 6
β’ ((π
β Ring β§ π₯ β π) β (opprβπ
) β SRing) |
58 | | eqidd 2178 |
. . . . . 6
β’ ((π
β Ring β§ π₯ β π) β
(.rβ(opprβπ
)) =
(.rβ(opprβπ
))) |
59 | 53, 46, 57, 58, 40 | dvdsr2d 13262 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (π₯(β₯rβ(opprβπ
))(1rβπ
) β βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
))) |
60 | 50, 59 | anbi12d 473 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β ((π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
)) β (βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) =
(1rβπ
) β§ βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
)))) |
61 | | reeanv 2646 |
. . . . 5
β’
(βπ¦ β
(Baseβπ
)βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)) β (βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯)
= (1rβπ
) β§
βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
))) |
62 | | eqidd 2178 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (Baseβπ
) = (Baseβπ
)) |
63 | | eqidd 2178 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (β₯rβπ
) = (β₯rβπ
)) |
64 | 38 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π
β SRing) |
65 | | eqidd 2178 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (.rβπ
) = (.rβπ
)) |
66 | | simprl 529 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π β (Baseβπ
)) |
67 | 40 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π₯ β (Baseβπ
)) |
68 | 62, 63, 64, 65, 66, 67 | dvdsrmuld 13263 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π(β₯rβπ
)(π₯(.rβπ
)π)) |
69 | | simplll 533 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π
β Ring) |
70 | | simplr 528 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦ β (Baseβπ
)) |
71 | 31, 8 | ringass 13197 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ (π¦ β (Baseβπ
) β§ π₯ β (Baseβπ
) β§ π β (Baseβπ
))) β ((π¦(.rβπ
)π₯)(.rβπ
)π) = (π¦(.rβπ
)(π₯(.rβπ
)π))) |
72 | 69, 70, 67, 66, 71 | syl13anc 1240 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((π¦(.rβπ
)π₯)(.rβπ
)π)
= (π¦(.rβπ
)(π₯(.rβπ
)π))) |
73 | | simprrl 539 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)π₯)
= (1rβπ
)) |
74 | 73 | oveq1d 5889 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((π¦(.rβπ
)π₯)(.rβπ
)π)
= ((1rβπ
)(.rβπ
)π)) |
75 | 39 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π₯ β π) |
76 | | eqid 2177 |
. . . . . . . . . . . . . . . . 17
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
77 | 31, 8, 51, 76 | opprmulg 13241 |
. . . . . . . . . . . . . . . 16
β’ ((π
β Ring β§ π β (Baseβπ
) β§ π₯ β π) β (π(.rβ(opprβπ
))π₯) = (π₯(.rβπ
)π)) |
78 | 69, 66, 75, 77 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π(.rβ(opprβπ
))π₯) = (π₯(.rβπ
)π)) |
79 | | simprrr 540 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π(.rβ(opprβπ
))π₯) = (1rβπ
)) |
80 | 78, 79 | eqtr3d 2212 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π₯(.rβπ
)π)
= (1rβπ
)) |
81 | 80 | oveq2d 5890 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)(π₯(.rβπ
)π)) = (π¦(.rβπ
)(1rβπ
))) |
82 | 72, 74, 81 | 3eqtr3d 2218 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((1rβπ
)(.rβπ
)π)
= (π¦(.rβπ
)(1rβπ
))) |
83 | 31, 8, 34 | ringlidm 13204 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π β (Baseβπ
)) β
((1rβπ
)(.rβπ
)π) = π) |
84 | 69, 66, 83 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((1rβπ
)(.rβπ
)π)
= π) |
85 | 31, 8, 34 | ringridm 13205 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π¦ β (Baseβπ
)) β (π¦(.rβπ
)(1rβπ
)) = π¦) |
86 | 69, 70, 85 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)(1rβπ
)) = π¦) |
87 | 82, 84, 86 | 3eqtr3d 2218 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π = π¦) |
88 | 68, 87, 80 | 3brtr3d 4034 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβπ
)(1rβπ
)) |
89 | 69, 52 | syl 14 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (Baseβπ
) = (Baseβ(opprβπ
))) |
90 | | eqidd 2178 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
))) |
91 | 69, 56 | syl 14 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (opprβπ
) β SRing) |
92 | | eqidd 2178 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β
(.rβ(opprβπ
)) =
(.rβ(opprβπ
))) |
93 | 89, 90, 91, 92, 70, 67 | dvdsrmuld 13263 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβ(opprβπ
))(π₯(.rβ(opprβπ
))π¦)) |
94 | 31, 8, 51, 76 | opprmulg 13241 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π₯ β π β§ π¦ β (Baseβπ
)) β (π₯(.rβ(opprβπ
))π¦) = (π¦(.rβπ
)π₯)) |
95 | 69, 75, 70, 94 | syl3anc 1238 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π₯(.rβ(opprβπ
))π¦) = (π¦(.rβπ
)π₯)) |
96 | 95, 73 | eqtrd 2210 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π₯(.rβ(opprβπ
))π¦) = (1rβπ
)) |
97 | 93, 96 | breqtrd 4029 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβ(opprβπ
))(1rβπ
)) |
98 | 1 | a1i 9 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π = (Unitβπ
)) |
99 | | eqidd 2178 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (1rβπ
) = (1rβπ
)) |
100 | | eqidd 2178 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (opprβπ
) = (opprβπ
)) |
101 | 98, 99, 63, 100, 90, 64 | isunitd 13273 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦ β π β (π¦(β₯rβπ
)(1rβπ
) β§ π¦(β₯rβ(opprβπ
))(1rβπ
)))) |
102 | 88, 97, 101 | mpbir2and 944 |
. . . . . . . . 9
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦ β π) |
103 | 102, 73 | jca 306 |
. . . . . . . 8
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦ β π β§ (π¦(.rβπ
)π₯)
= (1rβπ
))) |
104 | 103 | rexlimdvaa 2595 |
. . . . . . 7
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β (βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)) β (π¦ β π β§ (π¦(.rβπ
)π₯)
= (1rβπ
)))) |
105 | 104 | expimpd 363 |
. . . . . 6
β’ ((π
β Ring β§ π₯ β π) β ((π¦ β (Baseβπ
) β§ βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
))) β (π¦ β π β§ (π¦(.rβπ
)π₯)
= (1rβπ
)))) |
106 | 105 | reximdv2 2576 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (βπ¦ β (Baseβπ
)βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)) β βπ¦ β π (π¦(.rβπ
)π₯)
= (1rβπ
))) |
107 | 61, 106 | biimtrrid 153 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β ((βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
) β§ βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
)) β βπ¦ β π (π¦(.rβπ
)π₯)
= (1rβπ
))) |
108 | 60, 107 | sylbid 150 |
. . 3
β’ ((π
β Ring β§ π₯ β π) β ((π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
)) β βπ¦ β π
(π¦(.rβπ
)π₯) =
(1rβπ
))) |
109 | 48, 108 | mpd 13 |
. 2
β’ ((π
β Ring β§ π₯ β π) β βπ¦ β π (π¦(.rβπ
)π₯) = (1rβπ
)) |
110 | 6, 19, 20, 33, 35, 42, 109 | isgrpde 12897 |
1
β’ (π
β Ring β πΊ β Grp) |