Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . 3
β’
(Baseβπ
) =
(Baseβπ
) |
2 | 1 | subrgss 13281 |
. 2
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
3 | | eqid 2177 |
. . 3
β’
(1rβπ
) = (1rβπ
) |
4 | 3 | subrg1cl 13288 |
. 2
β’ (π΄ β (SubRingβπ
) β
(1rβπ
)
β π΄) |
5 | | subrgrcl 13285 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
6 | | eqid 2177 |
. . . . 5
β’ (π
βΎs π΄) = (π
βΎs π΄) |
7 | | subrgsubm.1 |
. . . . 5
β’ π = (mulGrpβπ
) |
8 | 6, 7 | mgpress 13072 |
. . . 4
β’ ((π
β Ring β§ π΄ β (SubRingβπ
)) β (π βΎs π΄) = (mulGrpβ(π
βΎs π΄))) |
9 | 5, 8 | mpancom 422 |
. . 3
β’ (π΄ β (SubRingβπ
) β (π βΎs π΄) = (mulGrpβ(π
βΎs π΄))) |
10 | 6 | subrgring 13283 |
. . . 4
β’ (π΄ β (SubRingβπ
) β (π
βΎs π΄) β Ring) |
11 | | eqid 2177 |
. . . . 5
β’
(mulGrpβ(π
βΎs π΄)) =
(mulGrpβ(π
βΎs π΄)) |
12 | 11 | ringmgp 13116 |
. . . 4
β’ ((π
βΎs π΄) β Ring β
(mulGrpβ(π
βΎs π΄))
β Mnd) |
13 | 10, 12 | syl 14 |
. . 3
β’ (π΄ β (SubRingβπ
) β (mulGrpβ(π
βΎs π΄)) β Mnd) |
14 | 9, 13 | eqeltrd 2254 |
. 2
β’ (π΄ β (SubRingβπ
) β (π βΎs π΄) β Mnd) |
15 | 7 | ringmgp 13116 |
. . . . 5
β’ (π
β Ring β π β Mnd) |
16 | | eqid 2177 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
17 | | eqid 2177 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
18 | | eqid 2177 |
. . . . . 6
β’ (π βΎs π΄) = (π βΎs π΄) |
19 | 16, 17, 18 | issubm2 12796 |
. . . . 5
β’ (π β Mnd β (π΄ β (SubMndβπ) β (π΄ β (Baseβπ) β§ (0gβπ) β π΄ β§ (π βΎs π΄) β Mnd))) |
20 | 15, 19 | syl 14 |
. . . 4
β’ (π
β Ring β (π΄ β (SubMndβπ) β (π΄ β (Baseβπ) β§ (0gβπ) β π΄ β§ (π βΎs π΄) β Mnd))) |
21 | 5, 20 | syl 14 |
. . 3
β’ (π΄ β (SubRingβπ
) β (π΄ β (SubMndβπ) β (π΄ β (Baseβπ) β§ (0gβπ) β π΄ β§ (π βΎs π΄) β Mnd))) |
22 | 7, 1 | mgpbasg 13067 |
. . . . . . 7
β’ (π
β Ring β
(Baseβπ
) =
(Baseβπ)) |
23 | 22 | sseq2d 3185 |
. . . . . 6
β’ (π
β Ring β (π΄ β (Baseβπ
) β π΄ β (Baseβπ))) |
24 | 7, 3 | ringidvalg 13075 |
. . . . . . 7
β’ (π
β Ring β
(1rβπ
) =
(0gβπ)) |
25 | 24 | eleq1d 2246 |
. . . . . 6
β’ (π
β Ring β
((1rβπ
)
β π΄ β
(0gβπ)
β π΄)) |
26 | 23, 25 | 3anbi12d 1313 |
. . . . 5
β’ (π
β Ring β ((π΄ β (Baseβπ
) β§
(1rβπ
)
β π΄ β§ (π βΎs π΄) β Mnd) β (π΄ β (Baseβπ) β§
(0gβπ)
β π΄ β§ (π βΎs π΄) β Mnd))) |
27 | 26 | bibi2d 232 |
. . . 4
β’ (π
β Ring β ((π΄ β (SubMndβπ) β (π΄ β (Baseβπ
) β§ (1rβπ
) β π΄ β§ (π βΎs π΄) β Mnd)) β (π΄ β (SubMndβπ) β (π΄ β (Baseβπ) β§ (0gβπ) β π΄ β§ (π βΎs π΄) β Mnd)))) |
28 | 5, 27 | syl 14 |
. . 3
β’ (π΄ β (SubRingβπ
) β ((π΄ β (SubMndβπ) β (π΄ β (Baseβπ
) β§ (1rβπ
) β π΄ β§ (π βΎs π΄) β Mnd)) β (π΄ β (SubMndβπ) β (π΄ β (Baseβπ) β§ (0gβπ) β π΄ β§ (π βΎs π΄) β Mnd)))) |
29 | 21, 28 | mpbird 167 |
. 2
β’ (π΄ β (SubRingβπ
) β (π΄ β (SubMndβπ) β (π΄ β (Baseβπ
) β§ (1rβπ
) β π΄ β§ (π βΎs π΄) β Mnd))) |
30 | 2, 4, 14, 29 | mpbir3and 1180 |
1
β’ (π΄ β (SubRingβπ
) β π΄ β (SubMndβπ)) |