Step | Hyp | Ref
| Expression |
1 | | invrvald.x |
. . . . 5
β’ (π β π β π΅) |
2 | | invrvald.y |
. . . . 5
β’ (π β π β π΅) |
3 | | invrvald.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
4 | | eqid 2733 |
. . . . . 6
β’
(β₯rβπ
) = (β₯rβπ
) |
5 | | invrvald.t |
. . . . . 6
β’ Β· =
(.rβπ
) |
6 | 3, 4, 5 | dvdsrmul 20085 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β π(β₯rβπ
)(π Β· π)) |
7 | 1, 2, 6 | syl2anc 585 |
. . . 4
β’ (π β π(β₯rβπ
)(π Β· π)) |
8 | | invrvald.yx |
. . . 4
β’ (π β (π Β· π) = 1 ) |
9 | 7, 8 | breqtrd 5135 |
. . 3
β’ (π β π(β₯rβπ
) 1 ) |
10 | | eqid 2733 |
. . . . . . 7
β’
(opprβπ
) = (opprβπ
) |
11 | 10, 3 | opprbas 20064 |
. . . . . 6
β’ π΅ =
(Baseβ(opprβπ
)) |
12 | | eqid 2733 |
. . . . . 6
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
13 | | eqid 2733 |
. . . . . 6
β’
(.rβ(opprβπ
)) =
(.rβ(opprβπ
)) |
14 | 11, 12, 13 | dvdsrmul 20085 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β π(β₯rβ(opprβπ
))(π(.rβ(opprβπ
))π)) |
15 | 1, 2, 14 | syl2anc 585 |
. . . 4
β’ (π β π(β₯rβ(opprβπ
))(π(.rβ(opprβπ
))π)) |
16 | 3, 5, 10, 13 | opprmul 20060 |
. . . . 5
β’ (π(.rβ(opprβπ
))π) = (π Β· π) |
17 | | invrvald.xy |
. . . . 5
β’ (π β (π Β· π) = 1 ) |
18 | 16, 17 | eqtrid 2785 |
. . . 4
β’ (π β (π(.rβ(opprβπ
))π) = 1 ) |
19 | 15, 18 | breqtrd 5135 |
. . 3
β’ (π β π(β₯rβ(opprβπ
)) 1 ) |
20 | | invrvald.u |
. . . 4
β’ π = (Unitβπ
) |
21 | | invrvald.o |
. . . 4
β’ 1 =
(1rβπ
) |
22 | 20, 21, 4, 10, 12 | isunit 20094 |
. . 3
β’ (π β π β (π(β₯rβπ
) 1 β§ π(β₯rβ(opprβπ
)) 1 )) |
23 | 9, 19, 22 | sylanbrc 584 |
. 2
β’ (π β π β π) |
24 | | invrvald.r |
. . . . 5
β’ (π β π
β Ring) |
25 | | eqid 2733 |
. . . . . 6
β’
((mulGrpβπ
)
βΎs π) =
((mulGrpβπ
)
βΎs π) |
26 | 20, 25, 21 | unitgrpid 20106 |
. . . . 5
β’ (π
β Ring β 1 =
(0gβ((mulGrpβπ
) βΎs π))) |
27 | 24, 26 | syl 17 |
. . . 4
β’ (π β 1 =
(0gβ((mulGrpβπ
) βΎs π))) |
28 | 17, 27 | eqtrd 2773 |
. . 3
β’ (π β (π Β· π) =
(0gβ((mulGrpβπ
) βΎs π))) |
29 | 20, 25 | unitgrp 20104 |
. . . . 5
β’ (π
β Ring β
((mulGrpβπ
)
βΎs π)
β Grp) |
30 | 24, 29 | syl 17 |
. . . 4
β’ (π β ((mulGrpβπ
) βΎs π) β Grp) |
31 | 3, 4, 5 | dvdsrmul 20085 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β π(β₯rβπ
)(π Β· π)) |
32 | 2, 1, 31 | syl2anc 585 |
. . . . . 6
β’ (π β π(β₯rβπ
)(π Β· π)) |
33 | 32, 17 | breqtrd 5135 |
. . . . 5
β’ (π β π(β₯rβπ
) 1 ) |
34 | 11, 12, 13 | dvdsrmul 20085 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β π(β₯rβ(opprβπ
))(π(.rβ(opprβπ
))π)) |
35 | 2, 1, 34 | syl2anc 585 |
. . . . . 6
β’ (π β π(β₯rβ(opprβπ
))(π(.rβ(opprβπ
))π)) |
36 | 3, 5, 10, 13 | opprmul 20060 |
. . . . . . 7
β’ (π(.rβ(opprβπ
))π) = (π Β· π) |
37 | 36, 8 | eqtrid 2785 |
. . . . . 6
β’ (π β (π(.rβ(opprβπ
))π) = 1 ) |
38 | 35, 37 | breqtrd 5135 |
. . . . 5
β’ (π β π(β₯rβ(opprβπ
)) 1 ) |
39 | 20, 21, 4, 10, 12 | isunit 20094 |
. . . . 5
β’ (π β π β (π(β₯rβπ
) 1 β§ π(β₯rβ(opprβπ
)) 1 )) |
40 | 33, 38, 39 | sylanbrc 584 |
. . . 4
β’ (π β π β π) |
41 | 20, 25 | unitgrpbas 20103 |
. . . . 5
β’ π =
(Baseβ((mulGrpβπ
) βΎs π)) |
42 | 20 | fvexi 6860 |
. . . . . 6
β’ π β V |
43 | | eqid 2733 |
. . . . . . . 8
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
44 | 43, 5 | mgpplusg 19908 |
. . . . . . 7
β’ Β· =
(+gβ(mulGrpβπ
)) |
45 | 25, 44 | ressplusg 17179 |
. . . . . 6
β’ (π β V β Β· =
(+gβ((mulGrpβπ
) βΎs π))) |
46 | 42, 45 | ax-mp 5 |
. . . . 5
β’ Β· =
(+gβ((mulGrpβπ
) βΎs π)) |
47 | | eqid 2733 |
. . . . 5
β’
(0gβ((mulGrpβπ
) βΎs π)) =
(0gβ((mulGrpβπ
) βΎs π)) |
48 | | invrvald.i |
. . . . . 6
β’ πΌ = (invrβπ
) |
49 | 20, 25, 48 | invrfval 20110 |
. . . . 5
β’ πΌ =
(invgβ((mulGrpβπ
) βΎs π)) |
50 | 41, 46, 47, 49 | grpinvid1 18810 |
. . . 4
β’
((((mulGrpβπ
)
βΎs π)
β Grp β§ π β
π β§ π β π) β ((πΌβπ) = π β (π Β· π) =
(0gβ((mulGrpβπ
) βΎs π)))) |
51 | 30, 23, 40, 50 | syl3anc 1372 |
. . 3
β’ (π β ((πΌβπ) = π β (π Β· π) =
(0gβ((mulGrpβπ
) βΎs π)))) |
52 | 28, 51 | mpbird 257 |
. 2
β’ (π β (πΌβπ) = π) |
53 | 23, 52 | jca 513 |
1
β’ (π β (π β π β§ (πΌβπ) = π)) |