Step | Hyp | Ref
| Expression |
1 | | subrgdv.1 |
. . . . . 6
β’ π = (π
βΎs π΄) |
2 | | eqid 2177 |
. . . . . 6
β’
(invrβπ
) = (invrβπ
) |
3 | | subrgdv.3 |
. . . . . 6
β’ π = (Unitβπ) |
4 | | eqid 2177 |
. . . . . 6
β’
(invrβπ) = (invrβπ) |
5 | 1, 2, 3, 4 | subrginv 13296 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((invrβπ
)βπ) = ((invrβπ)βπ)) |
6 | 5 | 3adant2 1016 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β ((invrβπ
)βπ) = ((invrβπ)βπ)) |
7 | 6 | oveq2d 5888 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (π(.rβπ
)((invrβπ
)βπ)) = (π(.rβπ
)((invrβπ)βπ))) |
8 | | subrgrcl 13285 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
9 | | eqid 2177 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
10 | 1, 9 | ressmulrg 12595 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π
β Ring) β
(.rβπ
) =
(.rβπ)) |
11 | 8, 10 | mpdan 421 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
12 | 11 | 3ad2ant1 1018 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (.rβπ
) = (.rβπ)) |
13 | 12 | oveqd 5889 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (π(.rβπ
)((invrβπ)βπ)) = (π(.rβπ)((invrβπ)βπ))) |
14 | 7, 13 | eqtrd 2210 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (π(.rβπ
)((invrβπ
)βπ)) = (π(.rβπ)((invrβπ)βπ))) |
15 | | eqidd 2178 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (Baseβπ
) = (Baseβπ
)) |
16 | | eqidd 2178 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (.rβπ
) = (.rβπ
)) |
17 | | eqidd 2178 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (Unitβπ
) = (Unitβπ
)) |
18 | | eqidd 2178 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (invrβπ
) = (invrβπ
)) |
19 | | subrgdv.2 |
. . . 4
β’ / =
(/rβπ
) |
20 | 19 | a1i 9 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β / =
(/rβπ
)) |
21 | 8 | 3ad2ant1 1018 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π
β Ring) |
22 | | eqid 2177 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
23 | 22 | subrgss 13281 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
24 | 23 | 3ad2ant1 1018 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π΄ β (Baseβπ
)) |
25 | | simp2 998 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π β π΄) |
26 | 24, 25 | sseldd 3156 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π β (Baseβπ
)) |
27 | | eqid 2177 |
. . . . . 6
β’
(Unitβπ
) =
(Unitβπ
) |
28 | 1, 27, 3 | subrguss 13295 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π β (Unitβπ
)) |
29 | 28 | 3ad2ant1 1018 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π β (Unitβπ
)) |
30 | | simp3 999 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π β π) |
31 | 29, 30 | sseldd 3156 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π β (Unitβπ
)) |
32 | 15, 16, 17, 18, 20, 21, 26, 31 | dvrvald 13234 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (π / π) = (π(.rβπ
)((invrβπ
)βπ))) |
33 | | eqidd 2178 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (Baseβπ) = (Baseβπ)) |
34 | | eqidd 2178 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (.rβπ) = (.rβπ)) |
35 | 3 | a1i 9 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π = (Unitβπ)) |
36 | | eqidd 2178 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (invrβπ) = (invrβπ)) |
37 | | subrgdv.4 |
. . . 4
β’ πΈ = (/rβπ) |
38 | 37 | a1i 9 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β πΈ = (/rβπ)) |
39 | 1 | subrgring 13283 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π β Ring) |
40 | 39 | 3ad2ant1 1018 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π β Ring) |
41 | 1 | subrgbas 13289 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
42 | 41 | 3ad2ant1 1018 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π΄ = (Baseβπ)) |
43 | 25, 42 | eleqtrd 2256 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β π β (Baseβπ)) |
44 | 33, 34, 35, 36, 38, 40, 43, 30 | dvrvald 13234 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (ππΈπ) = (π(.rβπ)((invrβπ)βπ))) |
45 | 14, 32, 44 | 3eqtr4d 2220 |
1
β’ ((π΄ β (SubRingβπ
) β§ π β π΄ β§ π β π) β (π / π) = (ππΈπ)) |