Step | Hyp | Ref
| Expression |
1 | | isdrng2.b |
. . 3
β’ π΅ = (Baseβπ
) |
2 | | eqid 2733 |
. . 3
β’
(Unitβπ
) =
(Unitβπ
) |
3 | | isdrng2.z |
. . 3
β’ 0 =
(0gβπ
) |
4 | 1, 2, 3 | isdrng 20223 |
. 2
β’ (π
β DivRing β (π
β Ring β§
(Unitβπ
) = (π΅ β { 0 }))) |
5 | | oveq2 7369 |
. . . . . . 7
β’
((Unitβπ
) =
(π΅ β { 0 }) β
((mulGrpβπ
)
βΎs (Unitβπ
)) = ((mulGrpβπ
) βΎs (π΅ β { 0 }))) |
6 | 5 | adantl 483 |
. . . . . 6
β’ ((π
β Ring β§
(Unitβπ
) = (π΅ β { 0 })) β
((mulGrpβπ
)
βΎs (Unitβπ
)) = ((mulGrpβπ
) βΎs (π΅ β { 0 }))) |
7 | | isdrng2.g |
. . . . . 6
β’ πΊ = ((mulGrpβπ
) βΎs (π΅ β { 0 })) |
8 | 6, 7 | eqtr4di 2791 |
. . . . 5
β’ ((π
β Ring β§
(Unitβπ
) = (π΅ β { 0 })) β
((mulGrpβπ
)
βΎs (Unitβπ
)) = πΊ) |
9 | | eqid 2733 |
. . . . . . 7
β’
((mulGrpβπ
)
βΎs (Unitβπ
)) = ((mulGrpβπ
) βΎs (Unitβπ
)) |
10 | 2, 9 | unitgrp 20104 |
. . . . . 6
β’ (π
β Ring β
((mulGrpβπ
)
βΎs (Unitβπ
)) β Grp) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π
β Ring β§
(Unitβπ
) = (π΅ β { 0 })) β
((mulGrpβπ
)
βΎs (Unitβπ
)) β Grp) |
12 | 8, 11 | eqeltrrd 2835 |
. . . 4
β’ ((π
β Ring β§
(Unitβπ
) = (π΅ β { 0 })) β πΊ β Grp) |
13 | 1, 2 | unitcl 20096 |
. . . . . . . . 9
β’ (π₯ β (Unitβπ
) β π₯ β π΅) |
14 | 13 | adantl 483 |
. . . . . . . 8
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β π₯ β π΅) |
15 | | difss 4095 |
. . . . . . . . . . . . . . 15
β’ (π΅ β { 0 }) β π΅ |
16 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
17 | 16, 1 | mgpbas 19910 |
. . . . . . . . . . . . . . . 16
β’ π΅ =
(Baseβ(mulGrpβπ
)) |
18 | 7, 17 | ressbas2 17128 |
. . . . . . . . . . . . . . 15
β’ ((π΅ β { 0 }) β π΅ β (π΅ β { 0 }) = (BaseβπΊ)) |
19 | 15, 18 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (π΅ β { 0 }) = (BaseβπΊ) |
20 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(0gβπΊ) = (0gβπΊ) |
21 | 19, 20 | grpidcl 18786 |
. . . . . . . . . . . . 13
β’ (πΊ β Grp β
(0gβπΊ)
β (π΅ β { 0
})) |
22 | 21 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β
(0gβπΊ)
β (π΅ β { 0
})) |
23 | | eldifsn 4751 |
. . . . . . . . . . . 12
β’
((0gβπΊ) β (π΅ β { 0 }) β
((0gβπΊ)
β π΅ β§
(0gβπΊ)
β 0
)) |
24 | 22, 23 | sylib 217 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β
((0gβπΊ)
β π΅ β§
(0gβπΊ)
β 0
)) |
25 | 24 | simprd 497 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β
(0gβπΊ)
β 0
) |
26 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β π
β Ring) |
27 | 22 | eldifad 3926 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β
(0gβπΊ)
β π΅) |
28 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β π₯ β (Unitβπ
)) |
29 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(/rβπ
) = (/rβπ
) |
30 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (.rβπ
) |
31 | 1, 2, 29, 30 | dvrcan1 20128 |
. . . . . . . . . . 11
β’ ((π
β Ring β§
(0gβπΊ)
β π΅ β§ π₯ β (Unitβπ
)) β
(((0gβπΊ)(/rβπ
)π₯)(.rβπ
)π₯) = (0gβπΊ)) |
32 | 26, 27, 28, 31 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β
(((0gβπΊ)(/rβπ
)π₯)(.rβπ
)π₯) = (0gβπΊ)) |
33 | 1, 2, 29 | dvrcl 20123 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§
(0gβπΊ)
β π΅ β§ π₯ β (Unitβπ
)) β
((0gβπΊ)(/rβπ
)π₯) β π΅) |
34 | 26, 27, 28, 33 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β
((0gβπΊ)(/rβπ
)π₯) β π΅) |
35 | 1, 30, 3 | ringrz 20020 |
. . . . . . . . . . 11
β’ ((π
β Ring β§
((0gβπΊ)(/rβπ
)π₯) β π΅) β (((0gβπΊ)(/rβπ
)π₯)(.rβπ
) 0 ) = 0 ) |
36 | 26, 34, 35 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β
(((0gβπΊ)(/rβπ
)π₯)(.rβπ
) 0 ) = 0 ) |
37 | 25, 32, 36 | 3netr4d 3018 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β
(((0gβπΊ)(/rβπ
)π₯)(.rβπ
)π₯) β (((0gβπΊ)(/rβπ
)π₯)(.rβπ
) 0 )) |
38 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π₯ = 0 β
(((0gβπΊ)(/rβπ
)π₯)(.rβπ
)π₯) = (((0gβπΊ)(/rβπ
)π₯)(.rβπ
) 0 )) |
39 | 38 | necon3i 2973 |
. . . . . . . . 9
β’
((((0gβπΊ)(/rβπ
)π₯)(.rβπ
)π₯) β (((0gβπΊ)(/rβπ
)π₯)(.rβπ
) 0 ) β π₯ β 0 ) |
40 | 37, 39 | syl 17 |
. . . . . . . 8
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β π₯ β 0 ) |
41 | | eldifsn 4751 |
. . . . . . . 8
β’ (π₯ β (π΅ β { 0 }) β (π₯ β π΅ β§ π₯ β 0 )) |
42 | 14, 40, 41 | sylanbrc 584 |
. . . . . . 7
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (Unitβπ
)) β π₯ β (π΅ β { 0 })) |
43 | 42 | ex 414 |
. . . . . 6
β’ ((π
β Ring β§ πΊ β Grp) β (π₯ β (Unitβπ
) β π₯ β (π΅ β { 0 }))) |
44 | 43 | ssrdv 3954 |
. . . . 5
β’ ((π
β Ring β§ πΊ β Grp) β
(Unitβπ
) β
(π΅ β { 0
})) |
45 | | eldifi 4090 |
. . . . . . . . 9
β’ (π₯ β (π΅ β { 0 }) β π₯ β π΅) |
46 | 45 | adantl 483 |
. . . . . . . 8
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β π₯ β π΅) |
47 | | eqid 2733 |
. . . . . . . . . . 11
β’
(invgβπΊ) = (invgβπΊ) |
48 | 19, 47 | grpinvcl 18806 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ π₯ β (π΅ β { 0 })) β
((invgβπΊ)βπ₯) β (π΅ β { 0 })) |
49 | 48 | adantll 713 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β
((invgβπΊ)βπ₯) β (π΅ β { 0 })) |
50 | 49 | eldifad 3926 |
. . . . . . . 8
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β
((invgβπΊ)βπ₯) β π΅) |
51 | | eqid 2733 |
. . . . . . . . 9
β’
(β₯rβπ
) = (β₯rβπ
) |
52 | 1, 51, 30 | dvdsrmul 20085 |
. . . . . . . 8
β’ ((π₯ β π΅ β§ ((invgβπΊ)βπ₯) β π΅) β π₯(β₯rβπ
)(((invgβπΊ)βπ₯)(.rβπ
)π₯)) |
53 | 46, 50, 52 | syl2anc 585 |
. . . . . . 7
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β π₯(β₯rβπ
)(((invgβπΊ)βπ₯)(.rβπ
)π₯)) |
54 | 1 | fvexi 6860 |
. . . . . . . . . . 11
β’ π΅ β V |
55 | | difexg 5288 |
. . . . . . . . . . 11
β’ (π΅ β V β (π΅ β { 0 }) β
V) |
56 | 16, 30 | mgpplusg 19908 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (+gβ(mulGrpβπ
)) |
57 | 7, 56 | ressplusg 17179 |
. . . . . . . . . . 11
β’ ((π΅ β { 0 }) β V β
(.rβπ
) =
(+gβπΊ)) |
58 | 54, 55, 57 | mp2b 10 |
. . . . . . . . . 10
β’
(.rβπ
) = (+gβπΊ) |
59 | 19, 58, 20, 47 | grplinv 18808 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π₯ β (π΅ β { 0 })) β
(((invgβπΊ)βπ₯)(.rβπ
)π₯) = (0gβπΊ)) |
60 | 59 | adantll 713 |
. . . . . . . 8
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β
(((invgβπΊ)βπ₯)(.rβπ
)π₯) = (0gβπΊ)) |
61 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(1rβπ
) = (1rβπ
) |
62 | 1, 61 | ringidcl 19997 |
. . . . . . . . . . . 12
β’ (π
β Ring β
(1rβπ
)
β π΅) |
63 | 1, 30, 61 | ringlidm 20000 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§
(1rβπ
)
β π΅) β
((1rβπ
)(.rβπ
)(1rβπ
)) = (1rβπ
)) |
64 | 62, 63 | mpdan 686 |
. . . . . . . . . . 11
β’ (π
β Ring β
((1rβπ
)(.rβπ
)(1rβπ
)) = (1rβπ
)) |
65 | 64 | adantr 482 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΊ β Grp) β
((1rβπ
)(.rβπ
)(1rβπ
)) = (1rβπ
)) |
66 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ πΊ β Grp) β πΊ β Grp) |
67 | 2, 61 | 1unit 20095 |
. . . . . . . . . . . . 13
β’ (π
β Ring β
(1rβπ
)
β (Unitβπ
)) |
68 | 67 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ πΊ β Grp) β
(1rβπ
)
β (Unitβπ
)) |
69 | 44, 68 | sseldd 3949 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ πΊ β Grp) β
(1rβπ
)
β (π΅ β { 0
})) |
70 | 19, 58, 20 | grpid 18794 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§
(1rβπ
)
β (π΅ β { 0 })) β
(((1rβπ
)(.rβπ
)(1rβπ
)) = (1rβπ
) β (0gβπΊ) = (1rβπ
))) |
71 | 66, 69, 70 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΊ β Grp) β
(((1rβπ
)(.rβπ
)(1rβπ
)) = (1rβπ
) β (0gβπΊ) = (1rβπ
))) |
72 | 65, 71 | mpbid 231 |
. . . . . . . . 9
β’ ((π
β Ring β§ πΊ β Grp) β
(0gβπΊ) =
(1rβπ
)) |
73 | 72 | adantr 482 |
. . . . . . . 8
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β
(0gβπΊ) =
(1rβπ
)) |
74 | 60, 73 | eqtrd 2773 |
. . . . . . 7
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β
(((invgβπΊ)βπ₯)(.rβπ
)π₯) = (1rβπ
)) |
75 | 53, 74 | breqtrd 5135 |
. . . . . 6
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β π₯(β₯rβπ
)(1rβπ
)) |
76 | | eqid 2733 |
. . . . . . . . . 10
β’
(opprβπ
) = (opprβπ
) |
77 | 76, 1 | opprbas 20064 |
. . . . . . . . 9
β’ π΅ =
(Baseβ(opprβπ
)) |
78 | | eqid 2733 |
. . . . . . . . 9
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
79 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
80 | 77, 78, 79 | dvdsrmul 20085 |
. . . . . . . 8
β’ ((π₯ β π΅ β§ ((invgβπΊ)βπ₯) β π΅) β π₯(β₯rβ(opprβπ
))(((invgβπΊ)βπ₯)(.rβ(opprβπ
))π₯)) |
81 | 46, 50, 80 | syl2anc 585 |
. . . . . . 7
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β π₯(β₯rβ(opprβπ
))(((invgβπΊ)βπ₯)(.rβ(opprβπ
))π₯)) |
82 | 1, 30, 76, 79 | opprmul 20060 |
. . . . . . . 8
β’
(((invgβπΊ)βπ₯)(.rβ(opprβπ
))π₯) = (π₯(.rβπ
)((invgβπΊ)βπ₯)) |
83 | 19, 58, 20, 47 | grprinv 18809 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ π₯ β (π΅ β { 0 })) β (π₯(.rβπ
)((invgβπΊ)βπ₯)) = (0gβπΊ)) |
84 | 83 | adantll 713 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β (π₯(.rβπ
)((invgβπΊ)βπ₯)) = (0gβπΊ)) |
85 | 84, 73 | eqtrd 2773 |
. . . . . . . 8
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β (π₯(.rβπ
)((invgβπΊ)βπ₯)) = (1rβπ
)) |
86 | 82, 85 | eqtrid 2785 |
. . . . . . 7
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β
(((invgβπΊ)βπ₯)(.rβ(opprβπ
))π₯) = (1rβπ
)) |
87 | 81, 86 | breqtrd 5135 |
. . . . . 6
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β π₯(β₯rβ(opprβπ
))(1rβπ
)) |
88 | 2, 61, 51, 76, 78 | isunit 20094 |
. . . . . 6
β’ (π₯ β (Unitβπ
) β (π₯(β₯rβπ
)(1rβπ
) β§ π₯(β₯rβ(opprβπ
))(1rβπ
))) |
89 | 75, 87, 88 | sylanbrc 584 |
. . . . 5
β’ (((π
β Ring β§ πΊ β Grp) β§ π₯ β (π΅ β { 0 })) β π₯ β (Unitβπ
)) |
90 | 44, 89 | eqelssd 3969 |
. . . 4
β’ ((π
β Ring β§ πΊ β Grp) β
(Unitβπ
) = (π΅ β { 0 })) |
91 | 12, 90 | impbida 800 |
. . 3
β’ (π
β Ring β
((Unitβπ
) = (π΅ β { 0 }) β πΊ β Grp)) |
92 | 91 | pm5.32i 576 |
. 2
β’ ((π
β Ring β§
(Unitβπ
) = (π΅ β { 0 })) β (π
β Ring β§ πΊ β Grp)) |
93 | 4, 92 | bitri 275 |
1
β’ (π
β DivRing β (π
β Ring β§ πΊ β Grp)) |