Step | Hyp | Ref
| Expression |
1 | | dvrass.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
2 | 1 | a1i 9 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π΅ = (Baseβπ
)) |
3 | | dvrass.t |
. . . . 5
β’ Β· =
(.rβπ
) |
4 | 3 | a1i 9 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β Β· =
(.rβπ
)) |
5 | | dvrass.o |
. . . . 5
β’ π = (Unitβπ
) |
6 | 5 | a1i 9 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π = (Unitβπ
)) |
7 | | eqid 2177 |
. . . . 5
β’
(invrβπ
) = (invrβπ
) |
8 | 7 | a1i 9 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (invrβπ
) = (invrβπ
)) |
9 | | dvrass.d |
. . . . 5
β’ / =
(/rβπ
) |
10 | 9 | a1i 9 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β / =
(/rβπ
)) |
11 | | simp1 997 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π
β Ring) |
12 | | simp2 998 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π β π΅) |
13 | | simp3 999 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π β π) |
14 | 2, 4, 6, 8, 10, 11, 12, 13 | dvrvald 13301 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (π / π) = (π Β·
((invrβπ
)βπ))) |
15 | 14 | oveq1d 5889 |
. 2
β’ ((π
β Ring β§ π β π΅ β§ π β π) β ((π / π) Β· π) = ((π Β·
((invrβπ
)βπ)) Β· π)) |
16 | 5, 7, 1 | ringinvcl 13292 |
. . . 4
β’ ((π
β Ring β§ π β π) β ((invrβπ
)βπ) β π΅) |
17 | 16 | 3adant2 1016 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β ((invrβπ
)βπ) β π΅) |
18 | | ringsrg 13222 |
. . . . 5
β’ (π
β Ring β π
β SRing) |
19 | 11, 18 | syl 14 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π
β SRing) |
20 | 2, 6, 19, 13 | unitcld 13275 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β π β π΅) |
21 | 1, 3 | ringass 13197 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ ((invrβπ
)βπ) β π΅ β§ π β π΅)) β ((π Β·
((invrβπ
)βπ)) Β· π) = (π Β·
(((invrβπ
)βπ) Β· π))) |
22 | 11, 12, 17, 20, 21 | syl13anc 1240 |
. 2
β’ ((π
β Ring β§ π β π΅ β§ π β π) β ((π Β·
((invrβπ
)βπ)) Β· π) = (π Β·
(((invrβπ
)βπ) Β· π))) |
23 | | eqid 2177 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
24 | 5, 7, 3, 23 | unitlinv 13293 |
. . . . 5
β’ ((π
β Ring β§ π β π) β (((invrβπ
)βπ) Β· π) = (1rβπ
)) |
25 | 24 | 3adant2 1016 |
. . . 4
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (((invrβπ
)βπ) Β· π) = (1rβπ
)) |
26 | 25 | oveq2d 5890 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (π Β·
(((invrβπ
)βπ) Β· π)) = (π Β·
(1rβπ
))) |
27 | 1, 3, 23 | ringridm 13205 |
. . . 4
β’ ((π
β Ring β§ π β π΅) β (π Β·
(1rβπ
)) =
π) |
28 | 27 | 3adant3 1017 |
. . 3
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (π Β·
(1rβπ
)) =
π) |
29 | 26, 28 | eqtrd 2210 |
. 2
β’ ((π
β Ring β§ π β π΅ β§ π β π) β (π Β·
(((invrβπ
)βπ) Β· π)) = π) |
30 | 15, 22, 29 | 3eqtrd 2214 |
1
β’ ((π
β Ring β§ π β π΅ β§ π β π) β ((π / π) Β· π) = π) |