Step | Hyp | Ref
| Expression |
1 | | istdrg2.m |
. . 3
β’ π = (mulGrpβπ
) |
2 | | eqid 2733 |
. . 3
β’
(Unitβπ
) =
(Unitβπ
) |
3 | 1, 2 | istdrg 23533 |
. 2
β’ (π
β TopDRing β (π
β TopRing β§ π
β DivRing β§ (π βΎs
(Unitβπ
)) β
TopGrp)) |
4 | | istdrg2.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ
) |
5 | | istdrg2.z |
. . . . . . . . 9
β’ 0 =
(0gβπ
) |
6 | 4, 2, 5 | isdrng 20201 |
. . . . . . . 8
β’ (π
β DivRing β (π
β Ring β§
(Unitβπ
) = (π΅ β { 0 }))) |
7 | 6 | simprbi 498 |
. . . . . . 7
β’ (π
β DivRing β
(Unitβπ
) = (π΅ β { 0 })) |
8 | 7 | adantl 483 |
. . . . . 6
β’ ((π
β TopRing β§ π
β DivRing) β
(Unitβπ
) = (π΅ β { 0 })) |
9 | 8 | oveq2d 7374 |
. . . . 5
β’ ((π
β TopRing β§ π
β DivRing) β (π βΎs
(Unitβπ
)) = (π βΎs (π΅ β { 0 }))) |
10 | 9 | eleq1d 2819 |
. . . 4
β’ ((π
β TopRing β§ π
β DivRing) β ((π βΎs
(Unitβπ
)) β
TopGrp β (π
βΎs (π΅
β { 0 })) β
TopGrp)) |
11 | 10 | pm5.32i 576 |
. . 3
β’ (((π
β TopRing β§ π
β DivRing) β§ (π βΎs
(Unitβπ
)) β
TopGrp) β ((π
β
TopRing β§ π
β
DivRing) β§ (π
βΎs (π΅
β { 0 })) β
TopGrp)) |
12 | | df-3an 1090 |
. . 3
β’ ((π
β TopRing β§ π
β DivRing β§ (π βΎs
(Unitβπ
)) β
TopGrp) β ((π
β
TopRing β§ π
β
DivRing) β§ (π
βΎs (Unitβπ
)) β TopGrp)) |
13 | | df-3an 1090 |
. . 3
β’ ((π
β TopRing β§ π
β DivRing β§ (π βΎs (π΅ β { 0 })) β TopGrp) β
((π
β TopRing β§
π
β DivRing) β§
(π βΎs
(π΅ β { 0 })) β
TopGrp)) |
14 | 11, 12, 13 | 3bitr4i 303 |
. 2
β’ ((π
β TopRing β§ π
β DivRing β§ (π βΎs
(Unitβπ
)) β
TopGrp) β (π
β
TopRing β§ π
β
DivRing β§ (π
βΎs (π΅
β { 0 })) β
TopGrp)) |
15 | 3, 14 | bitri 275 |
1
β’ (π
β TopDRing β (π
β TopRing β§ π
β DivRing β§ (π βΎs (π΅ β { 0 })) β
TopGrp)) |