Step | Hyp | Ref
| Expression |
1 | | unitmulcl.1 |
. . . 4
β’ π = (Unitβπ
) |
2 | | unitgrp.2 |
. . . 4
β’ πΊ = ((mulGrpβπ
) βΎs π) |
3 | 1, 2 | unitgrpbas 20096 |
. . 3
β’ π = (BaseβπΊ) |
4 | 3 | a1i 11 |
. 2
β’ (π
β Ring β π = (BaseβπΊ)) |
5 | 1 | fvexi 6857 |
. . 3
β’ π β V |
6 | | eqid 2737 |
. . . . 5
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
7 | | eqid 2737 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
8 | 6, 7 | mgpplusg 19901 |
. . . 4
β’
(.rβπ
) = (+gβ(mulGrpβπ
)) |
9 | 2, 8 | ressplusg 17172 |
. . 3
β’ (π β V β
(.rβπ
) =
(+gβπΊ)) |
10 | 5, 9 | mp1i 13 |
. 2
β’ (π
β Ring β
(.rβπ
) =
(+gβπΊ)) |
11 | 1, 7 | unitmulcl 20094 |
. 2
β’ ((π
β Ring β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
12 | | eqid 2737 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
13 | 12, 1 | unitcl 20089 |
. . . 4
β’ (π₯ β π β π₯ β (Baseβπ
)) |
14 | 12, 1 | unitcl 20089 |
. . . 4
β’ (π¦ β π β π¦ β (Baseβπ
)) |
15 | 12, 1 | unitcl 20089 |
. . . 4
β’ (π§ β π β π§ β (Baseβπ
)) |
16 | 13, 14, 15 | 3anim123i 1152 |
. . 3
β’ ((π₯ β π β§ π¦ β π β§ π§ β π) β (π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) |
17 | 12, 7 | ringass 19985 |
. . 3
β’ ((π
β Ring β§ (π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
) β§ π§ β (Baseβπ
))) β ((π₯(.rβπ
)π¦)(.rβπ
)π§) = (π₯(.rβπ
)(π¦(.rβπ
)π§))) |
18 | 16, 17 | sylan2 594 |
. 2
β’ ((π
β Ring β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯(.rβπ
)π¦)(.rβπ
)π§) = (π₯(.rβπ
)(π¦(.rβπ
)π§))) |
19 | | eqid 2737 |
. . 3
β’
(1rβπ
) = (1rβπ
) |
20 | 1, 19 | 1unit 20088 |
. 2
β’ (π
β Ring β
(1rβπ
)
β π) |
21 | 12, 7, 19 | ringlidm 19993 |
. . 3
β’ ((π
β Ring β§ π₯ β (Baseβπ
)) β
((1rβπ
)(.rβπ
)π₯) = π₯) |
22 | 13, 21 | sylan2 594 |
. 2
β’ ((π
β Ring β§ π₯ β π) β ((1rβπ
)(.rβπ
)π₯) = π₯) |
23 | | simpr 486 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β π₯ β π) |
24 | | eqid 2737 |
. . . . 5
β’
(β₯rβπ
) = (β₯rβπ
) |
25 | | eqid 2737 |
. . . . 5
β’
(opprβπ
) = (opprβπ
) |
26 | | eqid 2737 |
. . . . 5
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
27 | 1, 19, 24, 25, 26 | isunit 20087 |
. . . 4
β’ (π₯ β π β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
))) |
28 | 23, 27 | sylib 217 |
. . 3
β’ ((π
β Ring β§ π₯ β π) β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
))) |
29 | 13 | adantl 483 |
. . . . . 6
β’ ((π
β Ring β§ π₯ β π) β π₯ β (Baseβπ
)) |
30 | 12, 24, 7 | dvdsr2 20077 |
. . . . . 6
β’ (π₯ β (Baseβπ
) β (π₯(β₯rβπ
)(1rβπ
) β βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
))) |
31 | 29, 30 | syl 17 |
. . . . 5
β’ ((π
β Ring β§ π₯ β π) β (π₯(β₯rβπ
)(1rβπ
) β βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) = (1rβπ
))) |
32 | 25, 12 | opprbas 20057 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβ(opprβπ
)) |
33 | | eqid 2737 |
. . . . . . 7
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
34 | 32, 26, 33 | dvdsr2 20077 |
. . . . . 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 632 |
. . . 4
β’ ((π
β Ring β§ π₯ β π) β ((π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
)) β (βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯) =
(1rβπ
) β§ βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
)))) |
37 | | reeanv 3218 |
. . . . 5
β’
(βπ¦ β
(Baseβπ
)βπ β (Baseβπ
)((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)) β (βπ¦ β (Baseβπ
)(π¦(.rβπ
)π₯)
= (1rβπ
) β§
βπ β (Baseβπ
)(π(.rβ(opprβπ
))π₯) = (1rβπ
))) |
38 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π β (Baseβπ
)) |
39 | 29 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π₯ β (Baseβπ
)) |
40 | 12, 24, 7 | dvdsrmul 20078 |
. . . . . . . . . . . 12
β’ ((π β (Baseβπ
) β§ π₯ β (Baseβπ
)) β π(β₯rβπ
)(π₯(.rβπ
)π)) |
41 | 38, 39, 40 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π(β₯rβπ
)(π₯(.rβπ
)π)) |
42 | | simplll 774 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π
β Ring) |
43 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦ β (Baseβπ
)) |
44 | 12, 7 | ringass 19985 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ (π¦ β (Baseβπ
) β§ π₯ β (Baseβπ
) β§ π β (Baseβπ
))) β ((π¦(.rβπ
)π₯)(.rβπ
)π) = (π¦(.rβπ
)(π₯(.rβπ
)π))) |
45 | 42, 43, 39, 38, 44 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((π¦(.rβπ
)π₯)(.rβπ
)π)
= (π¦(.rβπ
)(π₯(.rβπ
)π))) |
46 | | simprrl 780 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)π₯)
= (1rβπ
)) |
47 | 46 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((π¦(.rβπ
)π₯)(.rβπ
)π)
= ((1rβπ
)(.rβπ
)π)) |
48 | 12, 7, 25, 33 | opprmul 20053 |
. . . . . . . . . . . . . . 15
β’ (π(.rβ(opprβπ
))π₯) = (π₯(.rβπ
)π) |
49 | | simprrr 781 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π(.rβ(opprβπ
))π₯) = (1rβπ
)) |
50 | 48, 49 | eqtr3id 2791 |
. . . . . . . . . . . . . 14
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π₯(.rβπ
)π)
= (1rβπ
)) |
51 | 50 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)(π₯(.rβπ
)π)) = (π¦(.rβπ
)(1rβπ
))) |
52 | 45, 47, 51 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((1rβπ
)(.rβπ
)π)
= (π¦(.rβπ
)(1rβπ
))) |
53 | 12, 7, 19 | ringlidm 19993 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π β (Baseβπ
)) β
((1rβπ
)(.rβπ
)π) = π) |
54 | 42, 38, 53 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β ((1rβπ
)(.rβπ
)π)
= π) |
55 | 12, 7, 19 | ringridm 19994 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π¦ β (Baseβπ
)) β (π¦(.rβπ
)(1rβπ
)) = π¦) |
56 | 42, 43, 55 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π¦(.rβπ
)(1rβπ
)) = π¦) |
57 | 52, 54, 56 | 3eqtr3d 2785 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π = π¦) |
58 | 41, 57, 50 | 3brtr3d 5137 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβπ
)(1rβπ
)) |
59 | 32, 26, 33 | dvdsrmul 20078 |
. . . . . . . . . . . 12
β’ ((π¦ β (Baseβπ
) β§ π₯ β (Baseβπ
)) β π¦(β₯rβ(opprβπ
))(π₯(.rβ(opprβπ
))π¦)) |
60 | 43, 39, 59 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβ(opprβπ
))(π₯(.rβ(opprβπ
))π¦)) |
61 | 12, 7, 25, 33 | opprmul 20053 |
. . . . . . . . . . . 12
β’ (π₯(.rβ(opprβπ
))π¦) = (π¦(.rβπ
)π₯) |
62 | 61, 46 | eqtrid 2789 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β (π₯(.rβ(opprβπ
))π¦) = (1rβπ
)) |
63 | 60, 62 | breqtrd 5132 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦(β₯rβ(opprβπ
))(1rβπ
)) |
64 | 1, 19, 24, 25, 26 | isunit 20087 |
. . . . . . . . . 10
β’ (π¦ β π β (π¦(β₯rβπ
)(1rβπ
) β§ π¦(β₯rβ(opprβπ
))(1rβπ
))) |
65 | 58, 63, 64 | sylanbrc 584 |
. . . . . . . . 9
β’ ((((π
β Ring β§ π₯ β π) β§ π¦ β (Baseβπ
)) β§ (π β (Baseβπ
) β§ ((π¦(.rβπ
)π₯) = (1rβπ
) β§ (π(.rβ(opprβπ
))π₯) = (1rβπ
)))) β π¦ β π) |
66 | 65, 46 | jca 513 |
. . . . . . . 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 455 |
. . . . . 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 18772 |
1
β’ (π
β Ring β πΊ β Grp) |