Step | Hyp | Ref
| Expression |
1 | | df-subrg 20262 |
. . 3
β’ SubRing =
(π β Ring β¦
{π β π«
(Baseβπ) β£
((π βΎs
π ) β Ring β§
(1rβπ)
β π )}) |
2 | 1 | mptrcl 6961 |
. 2
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
3 | | simpll 766 |
. 2
β’ (((π
β Ring β§ (π
βΎs π΄) β Ring) β§ (π΄ β π΅ β§ 1 β π΄)) β π
β Ring) |
4 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
5 | | issubrg.b |
. . . . . . . 8
β’ π΅ = (Baseβπ
) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . . 7
β’ (π = π
β (Baseβπ) = π΅) |
7 | 6 | pweqd 4581 |
. . . . . 6
β’ (π = π
β π« (Baseβπ) = π« π΅) |
8 | | oveq1 7368 |
. . . . . . . 8
β’ (π = π
β (π βΎs π ) = (π
βΎs π )) |
9 | 8 | eleq1d 2819 |
. . . . . . 7
β’ (π = π
β ((π βΎs π ) β Ring β (π
βΎs π ) β Ring)) |
10 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π
β (1rβπ) = (1rβπ
)) |
11 | | issubrg.i |
. . . . . . . . 9
β’ 1 =
(1rβπ
) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = π
β (1rβπ) = 1 ) |
13 | 12 | eleq1d 2819 |
. . . . . . 7
β’ (π = π
β ((1rβπ) β π β 1 β π )) |
14 | 9, 13 | anbi12d 632 |
. . . . . 6
β’ (π = π
β (((π βΎs π ) β Ring β§
(1rβπ)
β π ) β ((π
βΎs π ) β Ring β§ 1 β π ))) |
15 | 7, 14 | rabeqbidv 3423 |
. . . . 5
β’ (π = π
β {π β π« (Baseβπ) β£ ((π βΎs π ) β Ring β§
(1rβπ)
β π )} = {π β π« π΅ β£ ((π
βΎs π ) β Ring β§ 1 β π )}) |
16 | 5 | fvexi 6860 |
. . . . . . 7
β’ π΅ β V |
17 | 16 | pwex 5339 |
. . . . . 6
β’ π«
π΅ β V |
18 | 17 | rabex 5293 |
. . . . 5
β’ {π β π« π΅ β£ ((π
βΎs π ) β Ring β§ 1 β π )} β V |
19 | 15, 1, 18 | fvmpt 6952 |
. . . 4
β’ (π
β Ring β
(SubRingβπ
) = {π β π« π΅ β£ ((π
βΎs π ) β Ring β§ 1 β π )}) |
20 | 19 | eleq2d 2820 |
. . 3
β’ (π
β Ring β (π΄ β (SubRingβπ
) β π΄ β {π β π« π΅ β£ ((π
βΎs π ) β Ring β§ 1 β π )})) |
21 | | oveq2 7369 |
. . . . . . . 8
β’ (π = π΄ β (π
βΎs π ) = (π
βΎs π΄)) |
22 | 21 | eleq1d 2819 |
. . . . . . 7
β’ (π = π΄ β ((π
βΎs π ) β Ring β (π
βΎs π΄) β Ring)) |
23 | | eleq2 2823 |
. . . . . . 7
β’ (π = π΄ β ( 1 β π β 1 β π΄)) |
24 | 22, 23 | anbi12d 632 |
. . . . . 6
β’ (π = π΄ β (((π
βΎs π ) β Ring β§ 1 β π ) β ((π
βΎs π΄) β Ring β§ 1 β π΄))) |
25 | 24 | elrab 3649 |
. . . . 5
β’ (π΄ β {π β π« π΅ β£ ((π
βΎs π ) β Ring β§ 1 β π )} β (π΄ β π« π΅ β§ ((π
βΎs π΄) β Ring β§ 1 β π΄))) |
26 | 16 | elpw2 5306 |
. . . . . 6
β’ (π΄ β π« π΅ β π΄ β π΅) |
27 | 26 | anbi1i 625 |
. . . . 5
β’ ((π΄ β π« π΅ β§ ((π
βΎs π΄) β Ring β§ 1 β π΄)) β (π΄ β π΅ β§ ((π
βΎs π΄) β Ring β§ 1 β π΄))) |
28 | | an12 644 |
. . . . 5
β’ ((π΄ β π΅ β§ ((π
βΎs π΄) β Ring β§ 1 β π΄)) β ((π
βΎs π΄) β Ring β§ (π΄ β π΅ β§ 1 β π΄))) |
29 | 25, 27, 28 | 3bitri 297 |
. . . 4
β’ (π΄ β {π β π« π΅ β£ ((π
βΎs π ) β Ring β§ 1 β π )} β ((π
βΎs π΄) β Ring β§ (π΄ β π΅ β§ 1 β π΄))) |
30 | | ibar 530 |
. . . . 5
β’ (π
β Ring β ((π
βΎs π΄) β Ring β (π
β Ring β§ (π
βΎs π΄) β
Ring))) |
31 | 30 | anbi1d 631 |
. . . 4
β’ (π
β Ring β (((π
βΎs π΄) β Ring β§ (π΄ β π΅ β§ 1 β π΄)) β ((π
β Ring β§ (π
βΎs π΄) β Ring) β§ (π΄ β π΅ β§ 1 β π΄)))) |
32 | 29, 31 | bitrid 283 |
. . 3
β’ (π
β Ring β (π΄ β {π β π« π΅ β£ ((π
βΎs π ) β Ring β§ 1 β π )} β ((π
β Ring β§ (π
βΎs π΄) β Ring) β§ (π΄ β π΅ β§ 1 β π΄)))) |
33 | 20, 32 | bitrd 279 |
. 2
β’ (π
β Ring β (π΄ β (SubRingβπ
) β ((π
β Ring β§ (π
βΎs π΄) β Ring) β§ (π΄ β π΅ β§ 1 β π΄)))) |
34 | 2, 3, 33 | pm5.21nii 380 |
1
β’ (π΄ β (SubRingβπ
) β ((π
β Ring β§ (π
βΎs π΄) β Ring) β§ (π΄ β π΅ β§ 1 β π΄))) |