Step | Hyp | Ref
| Expression |
1 | | subrgrcl 13285 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
2 | 1 | adantr 276 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π
β Ring) |
3 | | subrginv.1 |
. . . . . . . 8
β’ π = (π
βΎs π΄) |
4 | 3 | subrgbas 13289 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
5 | | eqid 2177 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
6 | 5 | subrgss 13281 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
7 | 4, 6 | eqsstrrd 3192 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β (Baseβπ) β (Baseβπ
)) |
8 | 7 | adantr 276 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (Baseβπ) β (Baseβπ
)) |
9 | 3 | subrgring 13283 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β π β Ring) |
10 | | subrginv.3 |
. . . . . . 7
β’ π = (Unitβπ) |
11 | | subrginv.4 |
. . . . . . 7
β’ π½ = (invrβπ) |
12 | | eqid 2177 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
13 | 10, 11, 12 | ringinvcl 13225 |
. . . . . 6
β’ ((π β Ring β§ π β π) β (π½βπ) β (Baseβπ)) |
14 | 9, 13 | sylan 283 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (π½βπ) β (Baseβπ)) |
15 | 8, 14 | sseldd 3156 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (π½βπ) β (Baseβπ
)) |
16 | | eqidd 2178 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (Baseβπ) = (Baseβπ)) |
17 | 10 | a1i 9 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π = (Unitβπ)) |
18 | 9 | adantr 276 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β Ring) |
19 | | ringsrg 13155 |
. . . . . . 7
β’ (π β Ring β π β SRing) |
20 | 18, 19 | syl 14 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β SRing) |
21 | | simpr 110 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β π) |
22 | 16, 17, 20, 21 | unitcld 13208 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β (Baseβπ)) |
23 | 8, 22 | sseldd 3156 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β (Baseβπ
)) |
24 | | eqid 2177 |
. . . . . . 7
β’
(Unitβπ
) =
(Unitβπ
) |
25 | 3, 24, 10 | subrguss 13295 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β π β (Unitβπ
)) |
26 | 25 | sselda 3155 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π β π) β π β (Unitβπ
)) |
27 | | subrginv.2 |
. . . . . 6
β’ πΌ = (invrβπ
) |
28 | 24, 27, 5 | ringinvcl 13225 |
. . . . 5
β’ ((π
β Ring β§ π β (Unitβπ
)) β (πΌβπ) β (Baseβπ
)) |
29 | 1, 26, 28 | syl2an2r 595 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (πΌβπ) β (Baseβπ
)) |
30 | | eqid 2177 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
31 | 5, 30 | ringass 13130 |
. . . 4
β’ ((π
β Ring β§ ((π½βπ) β (Baseβπ
) β§ π β (Baseβπ
) β§ (πΌβπ) β (Baseβπ
))) β (((π½βπ)(.rβπ
)π)(.rβπ
)(πΌβπ)) = ((π½βπ)(.rβπ
)(π(.rβπ
)(πΌβπ)))) |
32 | 2, 15, 23, 29, 31 | syl13anc 1240 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (((π½βπ)(.rβπ
)π)(.rβπ
)(πΌβπ)) = ((π½βπ)(.rβπ
)(π(.rβπ
)(πΌβπ)))) |
33 | | eqid 2177 |
. . . . . . 7
β’
(.rβπ) = (.rβπ) |
34 | | eqid 2177 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
35 | 10, 11, 33, 34 | unitlinv 13226 |
. . . . . 6
β’ ((π β Ring β§ π β π) β ((π½βπ)(.rβπ)π) = (1rβπ)) |
36 | 9, 35 | sylan 283 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((π½βπ)(.rβπ)π) = (1rβπ)) |
37 | 3, 30 | ressmulrg 12595 |
. . . . . . . 8
β’ ((π΄ β (SubRingβπ
) β§ π
β Ring) β
(.rβπ
) =
(.rβπ)) |
38 | 1, 37 | mpdan 421 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
39 | 38 | adantr 276 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (.rβπ
) = (.rβπ)) |
40 | 39 | oveqd 5889 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((π½βπ)(.rβπ
)π) = ((π½βπ)(.rβπ)π)) |
41 | | eqid 2177 |
. . . . . . 7
β’
(1rβπ
) = (1rβπ
) |
42 | 3, 41 | subrg1 13290 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β
(1rβπ
) =
(1rβπ)) |
43 | 42 | adantr 276 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (1rβπ
) = (1rβπ)) |
44 | 36, 40, 43 | 3eqtr4d 2220 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((π½βπ)(.rβπ
)π) = (1rβπ
)) |
45 | 44 | oveq1d 5887 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (((π½βπ)(.rβπ
)π)(.rβπ
)(πΌβπ)) = ((1rβπ
)(.rβπ
)(πΌβπ))) |
46 | 24, 27, 30, 41 | unitrinv 13227 |
. . . . 5
β’ ((π
β Ring β§ π β (Unitβπ
)) β (π(.rβπ
)(πΌβπ)) = (1rβπ
)) |
47 | 1, 26, 46 | syl2an2r 595 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (π(.rβπ
)(πΌβπ)) = (1rβπ
)) |
48 | 47 | oveq2d 5888 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((π½βπ)(.rβπ
)(π(.rβπ
)(πΌβπ))) = ((π½βπ)(.rβπ
)(1rβπ
))) |
49 | 32, 45, 48 | 3eqtr3d 2218 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((1rβπ
)(.rβπ
)(πΌβπ)) = ((π½βπ)(.rβπ
)(1rβπ
))) |
50 | 5, 30, 41 | ringlidm 13137 |
. . 3
β’ ((π
β Ring β§ (πΌβπ) β (Baseβπ
)) β ((1rβπ
)(.rβπ
)(πΌβπ)) = (πΌβπ)) |
51 | 1, 29, 50 | syl2an2r 595 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((1rβπ
)(.rβπ
)(πΌβπ)) = (πΌβπ)) |
52 | 5, 30, 41 | ringridm 13138 |
. . 3
β’ ((π
β Ring β§ (π½βπ) β (Baseβπ
)) β ((π½βπ)(.rβπ
)(1rβπ
)) = (π½βπ)) |
53 | 1, 15, 52 | syl2an2r 595 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ π β π) β ((π½βπ)(.rβπ
)(1rβπ
)) = (π½βπ)) |
54 | 49, 51, 53 | 3eqtr3d 2218 |
1
β’ ((π΄ β (SubRingβπ
) β§ π β π) β (πΌβπ) = (π½βπ)) |