Step | Hyp | Ref
| Expression |
1 | | subrgsubg 20213 |
. . . . 5
β’ (π β (SubRingβπ
) β π β (SubGrpβπ
)) |
2 | 1 | ssriv 3946 |
. . . 4
β’
(SubRingβπ
)
β (SubGrpβπ
) |
3 | | sstr 3950 |
. . . 4
β’ ((π β (SubRingβπ
) β§ (SubRingβπ
) β (SubGrpβπ
)) β π β (SubGrpβπ
)) |
4 | 2, 3 | mpan2 689 |
. . 3
β’ (π β (SubRingβπ
) β π β (SubGrpβπ
)) |
5 | | subgint 18943 |
. . 3
β’ ((π β (SubGrpβπ
) β§ π β β
) β β© π
β (SubGrpβπ
)) |
6 | 4, 5 | sylan 580 |
. 2
β’ ((π β (SubRingβπ
) β§ π β β
) β β© π
β (SubGrpβπ
)) |
7 | | ssel2 3937 |
. . . . . 6
β’ ((π β (SubRingβπ
) β§ π β π) β π β (SubRingβπ
)) |
8 | 7 | adantlr 713 |
. . . . 5
β’ (((π β (SubRingβπ
) β§ π β β
) β§ π β π) β π β (SubRingβπ
)) |
9 | | eqid 2736 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
10 | 9 | subrg1cl 20215 |
. . . . 5
β’ (π β (SubRingβπ
) β
(1rβπ
)
β π) |
11 | 8, 10 | syl 17 |
. . . 4
β’ (((π β (SubRingβπ
) β§ π β β
) β§ π β π) β (1rβπ
) β π) |
12 | 11 | ralrimiva 3141 |
. . 3
β’ ((π β (SubRingβπ
) β§ π β β
) β βπ β π (1rβπ
) β π) |
13 | | fvex 6852 |
. . . 4
β’
(1rβπ
) β V |
14 | 13 | elint2 4912 |
. . 3
β’
((1rβπ
) β β© π β βπ β π (1rβπ
) β π) |
15 | 12, 14 | sylibr 233 |
. 2
β’ ((π β (SubRingβπ
) β§ π β β
) β
(1rβπ
)
β β© π) |
16 | 8 | adantlr 713 |
. . . . . 6
β’ ((((π β (SubRingβπ
) β§ π β β
) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β π β (SubRingβπ
)) |
17 | | simprl 769 |
. . . . . . 7
β’ (((π β (SubRingβπ
) β§ π β β
) β§ (π₯ β β© π β§ π¦ β β© π)) β π₯ β β© π) |
18 | | elinti 4914 |
. . . . . . . 8
β’ (π₯ β β© π
β (π β π β π₯ β π)) |
19 | 18 | imp 407 |
. . . . . . 7
β’ ((π₯ β β© π
β§ π β π) β π₯ β π) |
20 | 17, 19 | sylan 580 |
. . . . . 6
β’ ((((π β (SubRingβπ
) β§ π β β
) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β π₯ β π) |
21 | | simprr 771 |
. . . . . . 7
β’ (((π β (SubRingβπ
) β§ π β β
) β§ (π₯ β β© π β§ π¦ β β© π)) β π¦ β β© π) |
22 | | elinti 4914 |
. . . . . . . 8
β’ (π¦ β β© π
β (π β π β π¦ β π)) |
23 | 22 | imp 407 |
. . . . . . 7
β’ ((π¦ β β© π
β§ π β π) β π¦ β π) |
24 | 21, 23 | sylan 580 |
. . . . . 6
β’ ((((π β (SubRingβπ
) β§ π β β
) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β π¦ β π) |
25 | | eqid 2736 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
26 | 25 | subrgmcl 20219 |
. . . . . 6
β’ ((π β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
27 | 16, 20, 24, 26 | syl3anc 1371 |
. . . . 5
β’ ((((π β (SubRingβπ
) β§ π β β
) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β (π₯(.rβπ
)π¦) β π) |
28 | 27 | ralrimiva 3141 |
. . . 4
β’ (((π β (SubRingβπ
) β§ π β β
) β§ (π₯ β β© π β§ π¦ β β© π)) β βπ β π (π₯(.rβπ
)π¦) β π) |
29 | | ovex 7386 |
. . . . 5
β’ (π₯(.rβπ
)π¦) β V |
30 | 29 | elint2 4912 |
. . . 4
β’ ((π₯(.rβπ
)π¦) β β© π β βπ β π (π₯(.rβπ
)π¦) β π) |
31 | 28, 30 | sylibr 233 |
. . 3
β’ (((π β (SubRingβπ
) β§ π β β
) β§ (π₯ β β© π β§ π¦ β β© π)) β (π₯(.rβπ
)π¦) β β© π) |
32 | 31 | ralrimivva 3195 |
. 2
β’ ((π β (SubRingβπ
) β§ π β β
) β βπ₯ β β© πβπ¦ β β© π(π₯(.rβπ
)π¦) β β© π) |
33 | | ssn0 4358 |
. . 3
β’ ((π β (SubRingβπ
) β§ π β β
) β (SubRingβπ
) β β
) |
34 | | n0 4304 |
. . . 4
β’
((SubRingβπ
)
β β
β βπ π β (SubRingβπ
)) |
35 | | subrgrcl 20212 |
. . . . 5
β’ (π β (SubRingβπ
) β π
β Ring) |
36 | 35 | exlimiv 1933 |
. . . 4
β’
(βπ π β (SubRingβπ
) β π
β Ring) |
37 | 34, 36 | sylbi 216 |
. . 3
β’
((SubRingβπ
)
β β
β π
β Ring) |
38 | | eqid 2736 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
39 | 38, 9, 25 | issubrg2 20227 |
. . 3
β’ (π
β Ring β (β© π
β (SubRingβπ
)
β (β© π β (SubGrpβπ
) β§ (1rβπ
) β β© π
β§ βπ₯ β
β© πβπ¦ β β© π(π₯(.rβπ
)π¦) β β© π))) |
40 | 33, 37, 39 | 3syl 18 |
. 2
β’ ((π β (SubRingβπ
) β§ π β β
) β (β© π
β (SubRingβπ
)
β (β© π β (SubGrpβπ
) β§ (1rβπ
) β β© π
β§ βπ₯ β
β© πβπ¦ β β© π(π₯(.rβπ
)π¦) β β© π))) |
41 | 6, 15, 32, 40 | mpbir3and 1342 |
1
β’ ((π β (SubRingβπ
) β§ π β β
) β β© π
β (SubRingβπ
)) |