Step | Hyp | Ref
| Expression |
1 | | unitmulcl.1 |
. . . 4
β’ π = (Unitβπ
) |
2 | | unitgrp.2 |
. . . 4
β’ πΊ = ((mulGrpβπ
) βΎs π) |
3 | 1, 2 | unitgrpbas 20273 |
. . 3
β’ π = (BaseβπΊ) |
4 | 3 | a1i 11 |
. 2
β’ (π
β Ring β π = (BaseβπΊ)) |
5 | 1 | fvexi 6904 |
. . 3
β’ π β V |
6 | | eqid 2730 |
. . . . 5
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
7 | | eqid 2730 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
8 | 6, 7 | mgpplusg 20032 |
. . . 4
β’
(.rβπ
) = (+gβ(mulGrpβπ
)) |
9 | 2, 8 | ressplusg 17239 |
. . 3
β’ (π β V β
(.rβπ
) =
(+gβπΊ)) |
10 | 5, 9 | mp1i 13 |
. 2
β’ (π
β Ring β
(.rβπ
) =
(+gβπΊ)) |
11 | 1, 7 | unitmulcl 20271 |
. 2
β’ ((π
β Ring β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
12 | | eqid 2730 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
13 | 12, 1 | unitcl 20266 |
. . . 4
β’ (π₯ β π β π₯ β (Baseβπ
)) |
14 | 12, 1 | unitcl 20266 |
. . . 4
β’ (π¦ β π β π¦ β (Baseβπ
)) |
15 | 12, 1 | unitcl 20266 |
. . . 4
β’ (π§ β π β π§ β (Baseβπ
)) |
16 | 13, 14, 15 | 3anim123i 1149 |
. . 3
β’ ((π₯ β π β§ π¦ β π β§ π§ β π) β (π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) |
17 | 12, 7 | ringass 20147 |
. . 3
β’ ((π
β Ring β§ (π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) β ((π₯(.rβπ
)π¦)(.rβπ
)π§) = (π₯(.rβπ
)(π¦(.rβπ
)π§))) |
18 | 16, 17 | sylan2 591 |
. 2
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯(.rβπ
)π¦)(.rβπ
)π§) = (π₯(.rβπ
)(π¦(.rβπ
)π§))) |
19 | | eqid 2730 |
. . 3
β’
(1rβπ
) = (1rβπ
) |
20 | 1, 19 | 1unit 20265 |
. 2
β’ (π
β Ring β
(1rβπ
)
β π) |
21 | 12, 7, 19 | ringlidm 20157 |
. . 3
β’ ((π
β Ring β§ π₯ β (Baseβπ
)) β
((1rβπ
)(.rβπ
)π₯) = π₯) |
22 | 13, 21 | sylan2 591 |
. 2
β’ ((π
β Ring β§ π₯ β π) β ((1rβπ
)(.rβπ
)π₯) = π₯) |
23 | | simpr 483 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β π₯ β π) |
24 | | eqid 2730 |
. . . . 5
β’
(β₯rβπ
) = (β₯rβπ
) |
25 | | eqid 2730 |
. . . . 5
β’
(opprβπ
) = (opprβπ
) |
26 | | eqid 2730 |
. . . . 5
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
27 | 1, 19, 24, 25, 26 | isunit 20264 |
. . . 4
β’ (π₯ β π β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
))) |
28 | 23, 27 | sylib 217 |
. . 3
β’ ((π
β Ring β§ π₯ β π) β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
))) |
29 | 13 | adantl 480 |
. . . . . 6
β’ ((π
β Ring β§ π₯ β π) β π₯ β (Baseβπ
)) |
30 | 12, 24, 7 | dvdsr2 20254 |
. . . . . 6
β’ (π₯ β (Baseβπ
) β (π₯(β₯rβπ
)(1rβπ
) β βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
))) |
31 | 29, 30 | syl 17 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (π₯(β₯rβπ
)(1rβπ
) β βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
))) |
32 | 25, 12 | opprbas 20232 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβ(opprβπ
)) |
33 | | eqid 2730 |
. . . . . . 7
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
34 | 32, 26, 33 | dvdsr2 20254 |
. . . . . 6
β’ (π₯ β (Baseβπ
) β (π₯(β₯rβ(opprβπ
))(1rβπ
) β βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
))) |
35 | 29, 34 | syl 17 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (π₯(β₯rβ(opprβπ
))(1rβπ
) β βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
))) |
36 | 31, 35 | anbi12d 629 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β ((π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
)) β (βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) =
(1rβπ
) β§ βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
)))) |
37 | | reeanv 3224 |
. . . . 5
β’
(βπ¦ β
(Baseβπ
)βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)) β (βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯)
= (1rβπ
) β§
βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
))) |
38 | | simprl 767 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π β (Baseβπ
)) |
39 | 29 | ad2antrr 722 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π₯ β (Baseβπ
)) |
40 | 12, 24, 7 | dvdsrmul 20255 |
. . . . . . . . . . . 12
β’ ((π β (Baseβπ
) β§ π₯ β (Baseβπ
)) β π(β₯rβπ
)(π₯(.rβπ
)π)) |
41 | 38, 39, 40 | syl2anc 582 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π(β₯rβπ
)(π₯(.rβπ
)π)) |
42 | | simplll 771 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π
β Ring) |
43 | | simplr 765 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦ β (Baseβπ
)) |
44 | 12, 7 | ringass 20147 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ (π¦ β (Baseβπ
) β§ π₯ β (Baseβπ
) β§ π β (Baseβπ
))) β ((π¦(.rβπ
)π₯)(.rβπ
)π) = (π¦(.rβπ
)(π₯(.rβπ
)π))) |
45 | 42, 43, 39, 38, 44 | syl13anc 1370 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((π¦(.rβπ
)π₯)(.rβπ
)π)
= (π¦(.rβπ
)(π₯(.rβπ
)π))) |
46 | | simprrl 777 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)π₯)
= (1rβπ
)) |
47 | 46 | oveq1d 7426 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((π¦(.rβπ
)π₯)(.rβπ
)π)
= ((1rβπ
)(.rβπ
)π)) |
48 | 12, 7, 25, 33 | opprmul 20228 |
. . . . . . . . . . . . . . 15
β’ (π(.rβ(opprβπ
))π₯) = (π₯(.rβπ
)π) |
49 | | simprrr 778 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π(.rβ(opprβπ
))π₯) = (1rβπ
)) |
50 | 48, 49 | eqtr3id 2784 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π₯(.rβπ
)π)
= (1rβπ
)) |
51 | 50 | oveq2d 7427 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)(π₯(.rβπ
)π)) = (π¦(.rβπ
)(1rβπ
))) |
52 | 45, 47, 51 | 3eqtr3d 2778 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((1rβπ
)(.rβπ
)π)
= (π¦(.rβπ
)(1rβπ
))) |
53 | 12, 7, 19 | ringlidm 20157 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π β (Baseβπ
)) β
((1rβπ
)(.rβπ
)π) = π) |
54 | 42, 38, 53 | syl2anc 582 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((1rβπ
)(.rβπ
)π)
= π) |
55 | 12, 7, 19 | ringridm 20158 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π¦ β (Baseβπ
)) β (π¦(.rβπ
)(1rβπ
)) = π¦) |
56 | 42, 43, 55 | syl2anc 582 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)(1rβπ
)) = π¦) |
57 | 52, 54, 56 | 3eqtr3d 2778 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π = π¦) |
58 | 41, 57, 50 | 3brtr3d 5178 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβπ
)(1rβπ
)) |
59 | 32, 26, 33 | dvdsrmul 20255 |
. . . . . . . . . . . 12
β’ ((π¦ β (Baseβπ
) β§ π₯ β (Baseβπ
)) β π¦(β₯rβ(opprβπ
))(π₯(.rβ(opprβπ
))π¦)) |
60 | 43, 39, 59 | syl2anc 582 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβ(opprβπ
))(π₯(.rβ(opprβπ
))π¦)) |
61 | 12, 7, 25, 33 | opprmul 20228 |
. . . . . . . . . . . 12
β’ (π₯(.rβ(opprβπ
))π¦) = (π¦(.rβπ
)π₯) |
62 | 61, 46 | eqtrid 2782 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π₯(.rβ(opprβπ
))π¦) = (1rβπ
)) |
63 | 60, 62 | breqtrd 5173 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβ(opprβπ
))(1rβπ
)) |
64 | 1, 19, 24, 25, 26 | isunit 20264 |
. . . . . . . . . 10
β’ (π¦ β π β (π¦(β₯rβπ
)(1rβπ
) β§ π¦(β₯rβ(opprβπ
))(1rβπ
))) |
65 | 58, 63, 64 | sylanbrc 581 |
. . . . . . . . 9
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦ β π) |
66 | 65, 46 | jca 510 |
. . . . . . . 8
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦ β π β§ (π¦(.rβπ
)π₯)
= (1rβπ
))) |
67 | 66 | rexlimdvaa 3154 |
. . . . . . 7
β’ (((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β (βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)) β (π¦ β π β§ (π¦(.rβπ
)π₯)
= (1rβπ
)))) |
68 | 67 | expimpd 452 |
. . . . . 6
β’ ((π
β Ring β§ π₯ β π) β ((π¦ β (Baseβπ
) β§ βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
))) β (π¦ β π β§ (π¦(.rβπ
)π₯)
= (1rβπ
)))) |
69 | 68 | reximdv2 3162 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (βπ¦ β (Baseβπ
)βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)) β βπ¦ β π (π¦(.rβπ
)π₯)
= (1rβπ
))) |
70 | 37, 69 | biimtrrid 242 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β ((βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
) β§ βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
)) β βπ¦ β π (π¦(.rβπ
)π₯)
= (1rβπ
))) |
71 | 36, 70 | sylbid 239 |
. . 3
β’ ((π
β Ring β§ π₯ β π) β ((π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
)) β βπ¦ β π
(π¦(.rβπ
)π₯) =
(1rβπ
))) |
72 | 28, 71 | mpd 15 |
. 2
β’ ((π
β Ring β§ π₯ β π) β βπ¦ β π (π¦(.rβπ
)π₯) = (1rβπ
)) |
73 | 4, 10, 11, 18, 20, 22, 72 | isgrpde 18879 |
1
β’ (π
β Ring β πΊ β Grp) |