Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | eqid 2177 |
. . . 4
β’
(1rβπ
) = (1rβπ
) |
3 | | eqid 2177 |
. . . 4
β’
(.rβπ
) = (.rβπ
) |
4 | 1, 2, 3 | issubrg2 13300 |
. . 3
β’ (π
β Ring β (π β (SubRingβπ
) β (π β (SubGrpβπ
) β§ (1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π))) |
5 | | 3anass 982 |
. . 3
β’ ((π β (SubGrpβπ
) β§
(1rβπ
)
β π β§
βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π) β (π β (SubGrpβπ
) β§ ((1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π))) |
6 | 4, 5 | bitrdi 196 |
. 2
β’ (π
β Ring β (π β (SubRingβπ
) β (π β (SubGrpβπ
) β§ ((1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π)))) |
7 | 1 | subgss 12965 |
. . . 4
β’ (π β (SubGrpβπ
) β π β (Baseβπ
)) |
8 | | issubrg3.m |
. . . . . . . . 9
β’ π = (mulGrpβπ
) |
9 | 8 | ringmgp 13116 |
. . . . . . . 8
β’ (π
β Ring β π β Mnd) |
10 | | eqid 2177 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
11 | | eqid 2177 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
12 | | eqid 2177 |
. . . . . . . . 9
β’
(+gβπ) = (+gβπ) |
13 | 10, 11, 12 | issubm 12795 |
. . . . . . . 8
β’ (π β Mnd β (π β (SubMndβπ) β (π β (Baseβπ) β§ (0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
14 | 9, 13 | syl 14 |
. . . . . . 7
β’ (π
β Ring β (π β (SubMndβπ) β (π β (Baseβπ) β§ (0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
15 | 8, 1 | mgpbasg 13067 |
. . . . . . . . 9
β’ (π
β Ring β
(Baseβπ
) =
(Baseβπ)) |
16 | 15 | sseq2d 3185 |
. . . . . . . 8
β’ (π
β Ring β (π β (Baseβπ
) β π β (Baseβπ))) |
17 | 8, 2 | ringidvalg 13075 |
. . . . . . . . 9
β’ (π
β Ring β
(1rβπ
) =
(0gβπ)) |
18 | 17 | eleq1d 2246 |
. . . . . . . 8
β’ (π
β Ring β
((1rβπ
)
β π β
(0gβπ)
β π)) |
19 | 8, 3 | mgpplusgg 13065 |
. . . . . . . . . . 11
β’ (π
β Ring β
(.rβπ
) =
(+gβπ)) |
20 | 19 | oveqd 5889 |
. . . . . . . . . 10
β’ (π
β Ring β (π₯(.rβπ
)π¦) = (π₯(+gβπ)π¦)) |
21 | 20 | eleq1d 2246 |
. . . . . . . . 9
β’ (π
β Ring β ((π₯(.rβπ
)π¦) β π β (π₯(+gβπ)π¦) β π)) |
22 | 21 | 2ralbidv 2501 |
. . . . . . . 8
β’ (π
β Ring β
(βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π β βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) |
23 | 16, 18, 22 | 3anbi123d 1312 |
. . . . . . 7
β’ (π
β Ring β ((π β (Baseβπ
) β§
(1rβπ
)
β π β§
βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π) β (π β (Baseβπ) β§ (0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
24 | 14, 23 | bitr4d 191 |
. . . . . 6
β’ (π
β Ring β (π β (SubMndβπ) β (π β (Baseβπ
) β§ (1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π))) |
25 | | 3anass 982 |
. . . . . 6
β’ ((π β (Baseβπ
) β§
(1rβπ
)
β π β§
βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π) β (π β (Baseβπ
) β§ ((1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π))) |
26 | 24, 25 | bitrdi 196 |
. . . . 5
β’ (π
β Ring β (π β (SubMndβπ) β (π β (Baseβπ
) β§ ((1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π)))) |
27 | 26 | baibd 923 |
. . . 4
β’ ((π
β Ring β§ π β (Baseβπ
)) β (π β (SubMndβπ) β ((1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π))) |
28 | 7, 27 | sylan2 286 |
. . 3
β’ ((π
β Ring β§ π β (SubGrpβπ
)) β (π β (SubMndβπ) β ((1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π))) |
29 | 28 | pm5.32da 452 |
. 2
β’ (π
β Ring β ((π β (SubGrpβπ
) β§ π β (SubMndβπ)) β (π β (SubGrpβπ
) β§ ((1rβπ
) β π β§ βπ₯ β π βπ¦ β π (π₯(.rβπ
)π¦) β π)))) |
30 | 6, 29 | bitr4d 191 |
1
β’ (π
β Ring β (π β (SubRingβπ
) β (π β (SubGrpβπ
) β§ π β (SubMndβπ)))) |