Step | Hyp | Ref
| Expression |
1 | | dvrcan5.b |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
2 | | dvrcan5.o |
. . . . . . 7
β’ π = (Unitβπ
) |
3 | 1, 2 | unitss 20097 |
. . . . . 6
β’ π β π΅ |
4 | | simpr3 1197 |
. . . . . 6
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β π β π) |
5 | 3, 4 | sselid 3946 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β π β π΅) |
6 | | dvrcan5.t |
. . . . . . 7
β’ Β· =
(.rβπ
) |
7 | 2, 6 | unitmulcl 20101 |
. . . . . 6
β’ ((π
β Ring β§ π β π β§ π β π) β (π Β· π) β π) |
8 | 7 | 3adant3r1 1183 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β (π Β· π) β π) |
9 | | eqid 2733 |
. . . . . 6
β’
(invrβπ
) = (invrβπ
) |
10 | | dvrcan5.d |
. . . . . 6
β’ / =
(/rβπ
) |
11 | 1, 6, 2, 9, 10 | dvrval 20122 |
. . . . 5
β’ ((π β π΅ β§ (π Β· π) β π) β (π / (π Β· π)) = (π Β·
((invrβπ
)β(π Β· π)))) |
12 | 5, 8, 11 | syl2anc 585 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β (π / (π Β· π)) = (π Β·
((invrβπ
)β(π Β· π)))) |
13 | | simpl 484 |
. . . . . 6
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β π
β Ring) |
14 | | eqid 2733 |
. . . . . . 7
β’
((mulGrpβπ
)
βΎs π) =
((mulGrpβπ
)
βΎs π) |
15 | 2, 14 | unitgrp 20104 |
. . . . . 6
β’ (π
β Ring β
((mulGrpβπ
)
βΎs π)
β Grp) |
16 | 13, 15 | syl 17 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((mulGrpβπ
) βΎs π) β Grp) |
17 | | simpr2 1196 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β π β π) |
18 | 2, 14 | unitgrpbas 20103 |
. . . . . . 7
β’ π =
(Baseβ((mulGrpβπ
) βΎs π)) |
19 | 2 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
20 | | eqid 2733 |
. . . . . . . . . 10
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
21 | 20, 6 | mgpplusg 19908 |
. . . . . . . . 9
β’ Β· =
(+gβ(mulGrpβπ
)) |
22 | 14, 21 | ressplusg 17179 |
. . . . . . . 8
β’ (π β V β Β· =
(+gβ((mulGrpβπ
) βΎs π))) |
23 | 19, 22 | ax-mp 5 |
. . . . . . 7
β’ Β· =
(+gβ((mulGrpβπ
) βΎs π)) |
24 | 2, 14, 9 | invrfval 20110 |
. . . . . . 7
β’
(invrβπ
) =
(invgβ((mulGrpβπ
) βΎs π)) |
25 | 18, 23, 24 | grpinvadd 18833 |
. . . . . 6
β’
((((mulGrpβπ
)
βΎs π)
β Grp β§ π β
π β§ π β π) β ((invrβπ
)β(π Β· π)) = (((invrβπ
)βπ) Β·
((invrβπ
)βπ))) |
26 | 25 | oveq2d 7377 |
. . . . 5
β’
((((mulGrpβπ
)
βΎs π)
β Grp β§ π β
π β§ π β π) β (π Β·
((invrβπ
)β(π Β· π))) = (π Β·
(((invrβπ
)βπ) Β·
((invrβπ
)βπ)))) |
27 | 16, 17, 4, 26 | syl3anc 1372 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β (π Β·
((invrβπ
)β(π Β· π))) = (π Β·
(((invrβπ
)βπ) Β·
((invrβπ
)βπ)))) |
28 | | eqid 2733 |
. . . . . . . 8
β’
(1rβπ
) = (1rβπ
) |
29 | 2, 9, 6, 28 | unitrinv 20115 |
. . . . . . 7
β’ ((π
β Ring β§ π β π) β (π Β·
((invrβπ
)βπ)) = (1rβπ
)) |
30 | 29 | oveq1d 7376 |
. . . . . 6
β’ ((π
β Ring β§ π β π) β ((π Β·
((invrβπ
)βπ)) Β·
((invrβπ
)βπ)) = ((1rβπ
) Β·
((invrβπ
)βπ))) |
31 | 30 | 3ad2antr3 1191 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β·
((invrβπ
)βπ)) Β·
((invrβπ
)βπ)) = ((1rβπ
) Β·
((invrβπ
)βπ))) |
32 | 2, 9 | unitinvcl 20111 |
. . . . . . . 8
β’ ((π
β Ring β§ π β π) β ((invrβπ
)βπ) β π) |
33 | 32 | 3ad2antr3 1191 |
. . . . . . 7
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((invrβπ
)βπ) β π) |
34 | 3, 33 | sselid 3946 |
. . . . . 6
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((invrβπ
)βπ) β π΅) |
35 | 2, 9 | unitinvcl 20111 |
. . . . . . . 8
β’ ((π
β Ring β§ π β π) β ((invrβπ
)βπ) β π) |
36 | 35 | 3ad2antr2 1190 |
. . . . . . 7
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((invrβπ
)βπ) β π) |
37 | 3, 36 | sselid 3946 |
. . . . . 6
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((invrβπ
)βπ) β π΅) |
38 | 1, 6 | ringass 19992 |
. . . . . 6
β’ ((π
β Ring β§ (π β π΅ β§ ((invrβπ
)βπ) β π΅ β§ ((invrβπ
)βπ) β π΅)) β ((π Β·
((invrβπ
)βπ)) Β·
((invrβπ
)βπ)) = (π Β·
(((invrβπ
)βπ) Β·
((invrβπ
)βπ)))) |
39 | 13, 5, 34, 37, 38 | syl13anc 1373 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β·
((invrβπ
)βπ)) Β·
((invrβπ
)βπ)) = (π Β·
(((invrβπ
)βπ) Β·
((invrβπ
)βπ)))) |
40 | 1, 6, 28 | ringlidm 20000 |
. . . . . 6
β’ ((π
β Ring β§
((invrβπ
)βπ) β π΅) β ((1rβπ
) Β·
((invrβπ
)βπ)) = ((invrβπ
)βπ)) |
41 | 13, 37, 40 | syl2anc 585 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((1rβπ
) Β·
((invrβπ
)βπ)) = ((invrβπ
)βπ)) |
42 | 31, 39, 41 | 3eqtr3d 2781 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β (π Β·
(((invrβπ
)βπ) Β·
((invrβπ
)βπ))) = ((invrβπ
)βπ)) |
43 | 12, 27, 42 | 3eqtrd 2777 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β (π / (π Β· π)) = ((invrβπ
)βπ)) |
44 | 43 | oveq2d 7377 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β (π Β· (π / (π Β· π))) = (π Β·
((invrβπ
)βπ))) |
45 | | simpr1 1195 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β π β π΅) |
46 | 1, 2, 10, 6 | dvrass 20127 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ (π Β· π) β π)) β ((π Β· π) / (π Β· π)) = (π Β· (π / (π Β· π)))) |
47 | 13, 45, 5, 8, 46 | syl13anc 1373 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) / (π Β· π)) = (π Β· (π / (π Β· π)))) |
48 | 1, 6, 2, 9, 10 | dvrval 20122 |
. . 3
β’ ((π β π΅ β§ π β π) β (π / π) = (π Β·
((invrβπ
)βπ))) |
49 | 45, 17, 48 | syl2anc 585 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β (π / π) = (π Β·
((invrβπ
)βπ))) |
50 | 44, 47, 49 | 3eqtr4d 2783 |
1
β’ ((π
β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) / (π Β· π)) = (π / π)) |