Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π
β Ring) |
2 | | simpr1 1003 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π β π΅) |
3 | | simpr2 1004 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π β π΅) |
4 | | simpr3 1005 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π β π) |
5 | | dvrass.o |
. . . . 5
β’ π = (Unitβπ
) |
6 | | eqid 2177 |
. . . . 5
β’
(invrβπ
) = (invrβπ
) |
7 | | dvrass.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
8 | 5, 6, 7 | ringinvcl 13292 |
. . . 4
β’ ((π
β Ring β§ π β π) β ((invrβπ
)βπ) β π΅) |
9 | 4, 8 | syldan 282 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((invrβπ
)βπ) β π΅) |
10 | | dvrass.t |
. . . 4
β’ Β· =
(.rβπ
) |
11 | 7, 10 | ringass 13197 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ ((invrβπ
)βπ) β π΅)) β ((π Β· π) Β·
((invrβπ
)βπ)) = (π Β· (π Β·
((invrβπ
)βπ)))) |
12 | 1, 2, 3, 9, 11 | syl13anc 1240 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π Β· π) Β·
((invrβπ
)βπ)) = (π Β· (π Β·
((invrβπ
)βπ)))) |
13 | 7 | a1i 9 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π΅ = (Baseβπ
)) |
14 | 10 | a1i 9 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β Β· =
(.rβπ
)) |
15 | 5 | a1i 9 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β π = (Unitβπ
)) |
16 | 6 | a1i 9 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β (invrβπ
) = (invrβπ
)) |
17 | | dvrass.d |
. . . 4
β’ / =
(/rβπ
) |
18 | 17 | a1i 9 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β / =
(/rβπ
)) |
19 | 7, 10 | ringcl 13194 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π΅) β (π Β· π) β π΅) |
20 | 19 | 3adant3r3 1214 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π Β· π) β π΅) |
21 | 13, 14, 15, 16, 18, 1, 20, 4 | dvrvald 13301 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π Β· π) / π) = ((π Β· π) Β·
((invrβπ
)βπ))) |
22 | 13, 14, 15, 16, 18, 1, 3, 4 | dvrvald 13301 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π / π) = (π Β·
((invrβπ
)βπ))) |
23 | 22 | oveq2d 5890 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π Β· (π / π)) = (π Β· (π Β·
((invrβπ
)βπ)))) |
24 | 12, 21, 23 | 3eqtr4d 2220 |
1
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π Β· π) / π) = (π Β· (π / π))) |