Step | Hyp | Ref
| Expression |
1 | | subrg1.2 |
. 2
β’ 1 =
(1rβπ
) |
2 | | eqid 2177 |
. . . . 5
β’
(1rβπ
) = (1rβπ
) |
3 | 2 | subrg1cl 13288 |
. . . 4
β’ (π΄ β (SubRingβπ
) β
(1rβπ
)
β π΄) |
4 | | subrg1.1 |
. . . . 5
β’ π = (π
βΎs π΄) |
5 | 4 | subrgbas 13289 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
6 | 3, 5 | eleqtrd 2256 |
. . 3
β’ (π΄ β (SubRingβπ
) β
(1rβπ
)
β (Baseβπ)) |
7 | | eqid 2177 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
8 | 7 | subrgss 13281 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
9 | 5, 8 | eqsstrrd 3192 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β (Baseβπ) β (Baseβπ
)) |
10 | 9 | sselda 3155 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β (Baseβπ)) β π₯ β (Baseβπ
)) |
11 | | subrgrcl 13285 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
12 | | eqid 2177 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
13 | 7, 12, 2 | ringidmlem 13136 |
. . . . . . 7
β’ ((π
β Ring β§ π₯ β (Baseβπ
)) β
(((1rβπ
)(.rβπ
)π₯) = π₯ β§ (π₯(.rβπ
)(1rβπ
)) = π₯)) |
14 | 11, 13 | sylan 283 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β (Baseβπ
)) β (((1rβπ
)(.rβπ
)π₯) = π₯ β§ (π₯(.rβπ
)(1rβπ
)) = π₯)) |
15 | 4, 12 | ressmulrg 12595 |
. . . . . . . . . . 11
β’ ((π΄ β (SubRingβπ
) β§ π
β Ring) β
(.rβπ
) =
(.rβπ)) |
16 | 11, 15 | mpdan 421 |
. . . . . . . . . 10
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
17 | 16 | oveqd 5889 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β
((1rβπ
)(.rβπ
)π₯) = ((1rβπ
)(.rβπ)π₯)) |
18 | 17 | eqeq1d 2186 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(((1rβπ
)(.rβπ
)π₯) = π₯ β ((1rβπ
)(.rβπ)π₯) = π₯)) |
19 | 16 | oveqd 5889 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β (π₯(.rβπ
)(1rβπ
)) = (π₯(.rβπ)(1rβπ
))) |
20 | 19 | eqeq1d 2186 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β ((π₯(.rβπ
)(1rβπ
)) = π₯ β (π₯(.rβπ)(1rβπ
)) = π₯)) |
21 | 18, 20 | anbi12d 473 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β
((((1rβπ
)(.rβπ
)π₯) = π₯ β§ (π₯(.rβπ
)(1rβπ
)) = π₯) β (((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯))) |
22 | 21 | biimpa 296 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§
(((1rβπ
)(.rβπ
)π₯) = π₯ β§ (π₯(.rβπ
)(1rβπ
)) = π₯)) β (((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) |
23 | 14, 22 | syldan 282 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β (Baseβπ
)) β (((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) |
24 | 10, 23 | syldan 282 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π₯ β (Baseβπ)) β (((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) |
25 | 24 | ralrimiva 2550 |
. . 3
β’ (π΄ β (SubRingβπ
) β βπ₯ β (Baseβπ)(((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) |
26 | 4 | subrgring 13283 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π β Ring) |
27 | | eqid 2177 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
28 | | eqid 2177 |
. . . . 5
β’
(.rβπ) = (.rβπ) |
29 | | eqid 2177 |
. . . . 5
β’
(1rβπ) = (1rβπ) |
30 | 27, 28, 29 | isringid 13139 |
. . . 4
β’ (π β Ring β
(((1rβπ
)
β (Baseβπ) β§
βπ₯ β
(Baseβπ)(((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) β (1rβπ) = (1rβπ
))) |
31 | 26, 30 | syl 14 |
. . 3
β’ (π΄ β (SubRingβπ
) β
(((1rβπ
)
β (Baseβπ) β§
βπ₯ β
(Baseβπ)(((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) β (1rβπ) = (1rβπ
))) |
32 | 6, 25, 31 | mpbi2and 943 |
. 2
β’ (π΄ β (SubRingβπ
) β
(1rβπ) =
(1rβπ
)) |
33 | 1, 32 | eqtr4id 2229 |
1
β’ (π΄ β (SubRingβπ
) β 1 =
(1rβπ)) |