Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π
β Ring) |
2 | | simpr1 1194 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π β π΅) |
3 | | simpr2 1195 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π β π΅) |
4 | | dvrdir.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
5 | | dvrdir.u |
. . . . 5
β’ π = (Unitβπ
) |
6 | 4, 5 | unitss 20182 |
. . . 4
β’ π β π΅ |
7 | | simpr3 1196 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π β π) |
8 | | eqid 2732 |
. . . . . 6
β’
(invrβπ
) = (invrβπ
) |
9 | 5, 8 | unitinvcl 20196 |
. . . . 5
β’ ((π
β Ring β§ π β π) β ((invrβπ
)βπ) β π) |
10 | 7, 9 | syldan 591 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((invrβπ
)βπ) β π) |
11 | 6, 10 | sselid 3979 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((invrβπ
)βπ) β π΅) |
12 | | dvrdir.p |
. . . 4
β’ + =
(+gβπ
) |
13 | | eqid 2732 |
. . . 4
β’
(.rβπ
) = (.rβπ
) |
14 | 4, 12, 13 | ringdir 20075 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ ((invrβπ
)βπ) β π΅)) β ((π + π)(.rβπ
)((invrβπ
)βπ)) = ((π(.rβπ
)((invrβπ
)βπ)) + (π(.rβπ
)((invrβπ
)βπ)))) |
15 | 1, 2, 3, 11, 14 | syl13anc 1372 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π + π)(.rβπ
)((invrβπ
)βπ)) = ((π(.rβπ
)((invrβπ
)βπ)) + (π(.rβπ
)((invrβπ
)βπ)))) |
16 | | ringgrp 20054 |
. . . . 5
β’ (π
β Ring β π
β Grp) |
17 | 16 | adantr 481 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π
β Grp) |
18 | 4, 12 | grpcl 18823 |
. . . 4
β’ ((π
β Grp β§ π β π΅ β§ π β π΅) β (π + π) β π΅) |
19 | 17, 2, 3, 18 | syl3anc 1371 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π + π) β π΅) |
20 | | dvrdir.t |
. . . 4
β’ / =
(/rβπ
) |
21 | 4, 13, 5, 8, 20 | dvrval 20209 |
. . 3
β’ (((π + π) β π΅ β§ π β π) β ((π + π) / π) = ((π + π)(.rβπ
)((invrβπ
)βπ))) |
22 | 19, 7, 21 | syl2anc 584 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π + π) / π) = ((π + π)(.rβπ
)((invrβπ
)βπ))) |
23 | 4, 13, 5, 8, 20 | dvrval 20209 |
. . . 4
β’ ((π β π΅ β§ π β π) β (π / π) = (π(.rβπ
)((invrβπ
)βπ))) |
24 | 2, 7, 23 | syl2anc 584 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π / π) = (π(.rβπ
)((invrβπ
)βπ))) |
25 | 4, 13, 5, 8, 20 | dvrval 20209 |
. . . 4
β’ ((π β π΅ β§ π β π) β (π / π) = (π(.rβπ
)((invrβπ
)βπ))) |
26 | 3, 7, 25 | syl2anc 584 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π / π) = (π(.rβπ
)((invrβπ
)βπ))) |
27 | 24, 26 | oveq12d 7423 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π / π) + (π / π)) = ((π(.rβπ
)((invrβπ
)βπ)) + (π(.rβπ
)((invrβπ
)βπ)))) |
28 | 15, 22, 27 | 3eqtr4d 2782 |
1
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π + π) / π) = ((π / π) + (π / π))) |