Step | Hyp | Ref
| Expression |
1 | | subrg1.2 |
. 2
β’ 1 =
(1rβπ
) |
2 | | eqid 2733 |
. . . . 5
β’
(1rβπ
) = (1rβπ
) |
3 | 2 | subrg1cl 20244 |
. . . 4
β’ (π΄ β (SubRingβπ
) β
(1rβπ
)
β π΄) |
4 | | subrg1.1 |
. . . . 5
β’ π = (π
βΎs π΄) |
5 | 4 | subrgbas 20245 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
6 | 3, 5 | eleqtrd 2836 |
. . 3
β’ (π΄ β (SubRingβπ
) β
(1rβπ
)
β (Baseβπ)) |
7 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
8 | 7 | subrgss 20237 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
9 | 5, 8 | eqsstrrd 3984 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β (Baseβπ) β (Baseβπ
)) |
10 | 9 | sselda 3945 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β (Baseβπ)) β π₯ β (Baseβπ
)) |
11 | | subrgrcl 20241 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
13 | 7, 12, 2 | ringidmlem 19996 |
. . . . . . 7
β’ ((π
β Ring β§ π₯ β (Baseβπ
)) β
(((1rβπ
)(.rβπ
)π₯) = π₯ β§ (π₯(.rβπ
)(1rβπ
)) = π₯)) |
14 | 11, 13 | sylan 581 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π₯ β (Baseβπ
)) β (((1rβπ
)(.rβπ
)π₯) = π₯ β§ (π₯(.rβπ
)(1rβπ
)) = π₯)) |
15 | 4, 12 | ressmulr 17193 |
. . . . . . . . . 10
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
16 | 15 | oveqd 7375 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β
((1rβπ
)(.rβπ
)π₯) = ((1rβπ
)(.rβπ)π₯)) |
17 | 16 | eqeq1d 2735 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β
(((1rβπ
)(.rβπ
)π₯) = π₯ β ((1rβπ
)(.rβπ)π₯) = π₯)) |
18 | 15 | oveqd 7375 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β (π₯(.rβπ
)(1rβπ
)) = (π₯(.rβπ)(1rβπ
))) |
19 | 18 | eqeq1d 2735 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β ((π₯(.rβπ
)(1rβπ
)) = π₯ β (π₯(.rβπ)(1rβπ
)) = π₯)) |
20 | 17, 19 | anbi12d 632 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β
((((1rβπ
)(.rβπ
)π₯) = π₯ β§ (π₯(.rβπ
)(1rβπ
)) = π₯) β (((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯))) |
21 | 20 | biimpa 478 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§
(((1rβπ
)(.rβπ
)π₯) = π₯ β§ (π₯(.rβπ
)(1rβπ
)) = π₯)) β (((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) |
22 | 14, 21 | syldan 592 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π₯ β (Baseβπ
)) β (((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) |
23 | 10, 22 | syldan 592 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π₯ β (Baseβπ)) β (((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) |
24 | 23 | ralrimiva 3140 |
. . 3
β’ (π΄ β (SubRingβπ
) β βπ₯ β (Baseβπ)(((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) |
25 | 4 | subrgring 20239 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π β Ring) |
26 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
27 | | eqid 2733 |
. . . . 5
β’
(.rβπ) = (.rβπ) |
28 | | eqid 2733 |
. . . . 5
β’
(1rβπ) = (1rβπ) |
29 | 26, 27, 28 | isringid 19999 |
. . . 4
β’ (π β Ring β
(((1rβπ
)
β (Baseβπ) β§
βπ₯ β
(Baseβπ)(((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) β (1rβπ) = (1rβπ
))) |
30 | 25, 29 | syl 17 |
. . 3
β’ (π΄ β (SubRingβπ
) β
(((1rβπ
)
β (Baseβπ) β§
βπ₯ β
(Baseβπ)(((1rβπ
)(.rβπ)π₯) = π₯ β§ (π₯(.rβπ)(1rβπ
)) = π₯)) β (1rβπ) = (1rβπ
))) |
31 | 6, 24, 30 | mpbi2and 711 |
. 2
β’ (π΄ β (SubRingβπ
) β
(1rβπ) =
(1rβπ
)) |
32 | 1, 31 | eqtr4id 2792 |
1
β’ (π΄ β (SubRingβπ
) β 1 =
(1rβπ)) |