Step | Hyp | Ref
| Expression |
1 | | unitinvcl.1 |
. . . . . . 7
β’ π = (Unitβπ
) |
2 | 1 | a1i 9 |
. . . . . 6
β’ (π
β Ring β π = (Unitβπ
)) |
3 | | eqidd 2178 |
. . . . . 6
β’ (π
β Ring β
((mulGrpβπ
)
βΎs π) =
((mulGrpβπ
)
βΎs π)) |
4 | | ringsrg 13222 |
. . . . . 6
β’ (π
β Ring β π
β SRing) |
5 | 2, 3, 4 | unitgrpbasd 13282 |
. . . . 5
β’ (π
β Ring β π =
(Baseβ((mulGrpβπ
) βΎs π))) |
6 | 5 | eleq2d 2247 |
. . . 4
β’ (π
β Ring β (π β π β π β (Baseβ((mulGrpβπ
) βΎs π)))) |
7 | 6 | pm5.32i 454 |
. . 3
β’ ((π
β Ring β§ π β π) β (π
β Ring β§ π β (Baseβ((mulGrpβπ
) βΎs π)))) |
8 | | eqid 2177 |
. . . . 5
β’
((mulGrpβπ
)
βΎs π) =
((mulGrpβπ
)
βΎs π) |
9 | 1, 8 | unitgrp 13283 |
. . . 4
β’ (π
β Ring β
((mulGrpβπ
)
βΎs π)
β Grp) |
10 | | eqid 2177 |
. . . . 5
β’
(Baseβ((mulGrpβπ
) βΎs π)) = (Baseβ((mulGrpβπ
) βΎs π)) |
11 | | eqid 2177 |
. . . . 5
β’
(+gβ((mulGrpβπ
) βΎs π)) =
(+gβ((mulGrpβπ
) βΎs π)) |
12 | | eqid 2177 |
. . . . 5
β’
(0gβ((mulGrpβπ
) βΎs π)) =
(0gβ((mulGrpβπ
) βΎs π)) |
13 | | eqid 2177 |
. . . . 5
β’
(invgβ((mulGrpβπ
) βΎs π)) =
(invgβ((mulGrpβπ
) βΎs π)) |
14 | 10, 11, 12, 13 | grprinv 12922 |
. . . 4
β’
((((mulGrpβπ
)
βΎs π)
β Grp β§ π β
(Baseβ((mulGrpβπ
) βΎs π))) β (π(+gβ((mulGrpβπ
) βΎs π))((invgβ((mulGrpβπ
) βΎs π))βπ)) = (0gβ((mulGrpβπ
) βΎs π))) |
15 | 9, 14 | sylan 283 |
. . 3
β’ ((π
β Ring β§ π β
(Baseβ((mulGrpβπ
) βΎs π))) β (π(+gβ((mulGrpβπ
) βΎs π))((invgβ((mulGrpβπ
) βΎs π))βπ)) = (0gβ((mulGrpβπ
) βΎs π))) |
16 | 7, 15 | sylbi 121 |
. 2
β’ ((π
β Ring β§ π β π) β (π(+gβ((mulGrpβπ
) βΎs π))((invgβ((mulGrpβπ
) βΎs π))βπ)) = (0gβ((mulGrpβπ
) βΎs π))) |
17 | | eqid 2177 |
. . . . . 6
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
18 | | unitinvcl.3 |
. . . . . 6
β’ Β· =
(.rβπ
) |
19 | 17, 18 | mgpplusgg 13132 |
. . . . 5
β’ (π
β Ring β Β· =
(+gβ(mulGrpβπ
))) |
20 | | basfn 12519 |
. . . . . . 7
β’ Base Fn
V |
21 | | elex 2748 |
. . . . . . 7
β’ (π
β Ring β π
β V) |
22 | | funfvex 5532 |
. . . . . . . 8
β’ ((Fun
Base β§ π
β dom
Base) β (Baseβπ
)
β V) |
23 | 22 | funfni 5316 |
. . . . . . 7
β’ ((Base Fn
V β§ π
β V) β
(Baseβπ
) β
V) |
24 | 20, 21, 23 | sylancr 414 |
. . . . . 6
β’ (π
β Ring β
(Baseβπ
) β
V) |
25 | | eqidd 2178 |
. . . . . . 7
β’ (π
β Ring β
(Baseβπ
) =
(Baseβπ
)) |
26 | 25, 2, 4 | unitssd 13276 |
. . . . . 6
β’ (π
β Ring β π β (Baseβπ
)) |
27 | 24, 26 | ssexd 4143 |
. . . . 5
β’ (π
β Ring β π β V) |
28 | 17 | mgpex 13133 |
. . . . 5
β’ (π
β Ring β
(mulGrpβπ
) β
V) |
29 | 3, 19, 27, 28 | ressplusgd 12586 |
. . . 4
β’ (π
β Ring β Β· =
(+gβ((mulGrpβπ
) βΎs π))) |
30 | | eqidd 2178 |
. . . 4
β’ (π
β Ring β π = π) |
31 | | unitinvcl.2 |
. . . . . . 7
β’ πΌ = (invrβπ
) |
32 | 31 | a1i 9 |
. . . . . 6
β’ (π
β Ring β πΌ = (invrβπ
)) |
33 | | id 19 |
. . . . . 6
β’ (π
β Ring β π
β Ring) |
34 | 2, 3, 32, 33 | invrfvald 13289 |
. . . . 5
β’ (π
β Ring β πΌ =
(invgβ((mulGrpβπ
) βΎs π))) |
35 | 34 | fveq1d 5517 |
. . . 4
β’ (π
β Ring β (πΌβπ) =
((invgβ((mulGrpβπ
) βΎs π))βπ)) |
36 | 29, 30, 35 | oveq123d 5895 |
. . 3
β’ (π
β Ring β (π Β· (πΌβπ)) = (π(+gβ((mulGrpβπ
) βΎs π))((invgβ((mulGrpβπ
) βΎs π))βπ))) |
37 | 36 | adantr 276 |
. 2
β’ ((π
β Ring β§ π β π) β (π Β· (πΌβπ)) = (π(+gβ((mulGrpβπ
) βΎs π))((invgβ((mulGrpβπ
) βΎs π))βπ))) |
38 | | unitinvcl.4 |
. . . 4
β’ 1 =
(1rβπ
) |
39 | 1, 8, 38 | unitgrpid 13285 |
. . 3
β’ (π
β Ring β 1 =
(0gβ((mulGrpβπ
) βΎs π))) |
40 | 39 | adantr 276 |
. 2
β’ ((π
β Ring β§ π β π) β 1 =
(0gβ((mulGrpβπ
) βΎs π))) |
41 | 16, 37, 40 | 3eqtr4d 2220 |
1
β’ ((π
β Ring β§ π β π) β (π Β· (πΌβπ)) = 1 ) |