Step | Hyp | Ref
| Expression |
1 | | subrgsubg 13286 |
. . . . 5
β’ (π β (SubRingβπ
) β π β (SubGrpβπ
)) |
2 | 1 | ssriv 3159 |
. . . 4
β’
(SubRingβπ
)
β (SubGrpβπ
) |
3 | | sstr 3163 |
. . . 4
β’ ((π β (SubRingβπ
) β§ (SubRingβπ
) β (SubGrpβπ
)) β π β (SubGrpβπ
)) |
4 | 2, 3 | mpan2 425 |
. . 3
β’ (π β (SubRingβπ
) β π β (SubGrpβπ
)) |
5 | | subgintm 12989 |
. . 3
β’ ((π β (SubGrpβπ
) β§ βπ€ π€ β π) β β© π β (SubGrpβπ
)) |
6 | 4, 5 | sylan 283 |
. 2
β’ ((π β (SubRingβπ
) β§ βπ€ π€ β π) β β© π β (SubGrpβπ
)) |
7 | | ssel2 3150 |
. . . . . 6
β’ ((π β (SubRingβπ
) β§ π β π) β π β (SubRingβπ
)) |
8 | 7 | adantlr 477 |
. . . . 5
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ π β π) β π β (SubRingβπ
)) |
9 | | eqid 2177 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
10 | 9 | subrg1cl 13288 |
. . . . 5
β’ (π β (SubRingβπ
) β
(1rβπ
)
β π) |
11 | 8, 10 | syl 14 |
. . . 4
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ π β π) β (1rβπ
) β π) |
12 | 11 | ralrimiva 2550 |
. . 3
β’ ((π β (SubRingβπ
) β§ βπ€ π€ β π) β βπ β π (1rβπ
) β π) |
13 | | ssel 3149 |
. . . . . . 7
β’ (π β (SubRingβπ
) β (π€ β π β π€ β (SubRingβπ
))) |
14 | | subrgrcl 13285 |
. . . . . . 7
β’ (π€ β (SubRingβπ
) β π
β Ring) |
15 | 13, 14 | syl6 33 |
. . . . . 6
β’ (π β (SubRingβπ
) β (π€ β π β π
β Ring)) |
16 | 15 | exlimdv 1819 |
. . . . 5
β’ (π β (SubRingβπ
) β (βπ€ π€ β π β π
β Ring)) |
17 | 16 | imp 124 |
. . . 4
β’ ((π β (SubRingβπ
) β§ βπ€ π€ β π) β π
β Ring) |
18 | | ringsrg 13155 |
. . . 4
β’ (π
β Ring β π
β SRing) |
19 | | eqid 2177 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
20 | 19, 9 | srgidcl 13090 |
. . . . 5
β’ (π
β SRing β
(1rβπ
)
β (Baseβπ
)) |
21 | | elintg 3852 |
. . . . 5
β’
((1rβπ
) β (Baseβπ
) β ((1rβπ
) β β© π
β βπ β
π
(1rβπ
)
β π)) |
22 | 20, 21 | syl 14 |
. . . 4
β’ (π
β SRing β
((1rβπ
)
β β© π β βπ β π (1rβπ
) β π)) |
23 | 17, 18, 22 | 3syl 17 |
. . 3
β’ ((π β (SubRingβπ
) β§ βπ€ π€ β π) β ((1rβπ
) β β© π
β βπ β
π
(1rβπ
)
β π)) |
24 | 12, 23 | mpbird 167 |
. 2
β’ ((π β (SubRingβπ
) β§ βπ€ π€ β π) β (1rβπ
) β β© π) |
25 | 8 | adantlr 477 |
. . . . . 6
β’ ((((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β π β (SubRingβπ
)) |
26 | | simprl 529 |
. . . . . . 7
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β π₯ β β© π) |
27 | | elinti 3853 |
. . . . . . . 8
β’ (π₯ β β© π
β (π β π β π₯ β π)) |
28 | 27 | imp 124 |
. . . . . . 7
β’ ((π₯ β β© π
β§ π β π) β π₯ β π) |
29 | 26, 28 | sylan 283 |
. . . . . 6
β’ ((((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β π₯ β π) |
30 | | simprr 531 |
. . . . . . 7
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β π¦ β β© π) |
31 | | elinti 3853 |
. . . . . . . 8
β’ (π¦ β β© π
β (π β π β π¦ β π)) |
32 | 31 | imp 124 |
. . . . . . 7
β’ ((π¦ β β© π
β§ π β π) β π¦ β π) |
33 | 30, 32 | sylan 283 |
. . . . . 6
β’ ((((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β π¦ β π) |
34 | | eqid 2177 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
35 | 34 | subrgmcl 13292 |
. . . . . 6
β’ ((π β (SubRingβπ
) β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ
)π¦) β π) |
36 | 25, 29, 33, 35 | syl3anc 1238 |
. . . . 5
β’ ((((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β (π₯(.rβπ
)π¦) β π) |
37 | 36 | ralrimiva 2550 |
. . . 4
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β βπ β π (π₯(.rβπ
)π¦) β π) |
38 | | simplr 528 |
. . . . . 6
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β βπ€ π€ β π) |
39 | | eleq1w 2238 |
. . . . . . . 8
β’ (π = π€ β (π β π β π€ β π)) |
40 | 39 | cbvexv 1918 |
. . . . . . 7
β’
(βπ π β π β βπ€ π€ β π) |
41 | 36 | elexd 2750 |
. . . . . . . . 9
β’ ((((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β§ π β π) β (π₯(.rβπ
)π¦) β V) |
42 | 41 | ex 115 |
. . . . . . . 8
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β (π β π β (π₯(.rβπ
)π¦) β V)) |
43 | 42 | exlimdv 1819 |
. . . . . . 7
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β (βπ π β π β (π₯(.rβπ
)π¦) β V)) |
44 | 40, 43 | biimtrrid 153 |
. . . . . 6
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β (βπ€ π€ β π β (π₯(.rβπ
)π¦) β V)) |
45 | 38, 44 | mpd 13 |
. . . . 5
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β (π₯(.rβπ
)π¦) β V) |
46 | | elintg 3852 |
. . . . 5
β’ ((π₯(.rβπ
)π¦) β V β ((π₯(.rβπ
)π¦) β β© π β βπ β π (π₯(.rβπ
)π¦) β π)) |
47 | 45, 46 | syl 14 |
. . . 4
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β ((π₯(.rβπ
)π¦) β β© π β βπ β π (π₯(.rβπ
)π¦) β π)) |
48 | 37, 47 | mpbird 167 |
. . 3
β’ (((π β (SubRingβπ
) β§ βπ€ π€ β π) β§ (π₯ β β© π β§ π¦ β β© π)) β (π₯(.rβπ
)π¦) β β© π) |
49 | 48 | ralrimivva 2559 |
. 2
β’ ((π β (SubRingβπ
) β§ βπ€ π€ β π) β βπ₯ β β© πβπ¦ β β© π(π₯(.rβπ
)π¦) β β© π) |
50 | 19, 9, 34 | issubrg2 13300 |
. . 3
β’ (π
β Ring β (β© π
β (SubRingβπ
)
β (β© π β (SubGrpβπ
) β§ (1rβπ
) β β© π
β§ βπ₯ β
β© πβπ¦ β β© π(π₯(.rβπ
)π¦) β β© π))) |
51 | 17, 50 | syl 14 |
. 2
β’ ((π β (SubRingβπ
) β§ βπ€ π€ β π) β (β© π β (SubRingβπ
) β (β© π
β (SubGrpβπ
)
β§ (1rβπ
) β β© π β§ βπ₯ β β© πβπ¦ β β© π(π₯(.rβπ
)π¦) β β© π))) |
52 | 6, 24, 49, 51 | mpbir3and 1180 |
1
β’ ((π β (SubRingβπ
) β§ βπ€ π€ β π) β β© π β (SubRingβπ
)) |