MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  istdrg2 Structured version   Visualization version   GIF version

Theorem istdrg2 24102
Description: A topological-ring division ring is a topological division ring iff the group of nonzero elements is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
Hypotheses
Ref Expression
istdrg2.m 𝑀 = (mulGrpβ€˜π‘…)
istdrg2.b 𝐡 = (Baseβ€˜π‘…)
istdrg2.z 0 = (0gβ€˜π‘…)
Assertion
Ref Expression
istdrg2 (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))

Proof of Theorem istdrg2
StepHypRef Expression
1 istdrg2.m . . 3 𝑀 = (mulGrpβ€˜π‘…)
2 eqid 2728 . . 3 (Unitβ€˜π‘…) = (Unitβ€˜π‘…)
31, 2istdrg 24090 . 2 (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp))
4 istdrg2.b . . . . . . . . 9 𝐡 = (Baseβ€˜π‘…)
5 istdrg2.z . . . . . . . . 9 0 = (0gβ€˜π‘…)
64, 2, 5isdrng 20635 . . . . . . . 8 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unitβ€˜π‘…) = (𝐡 βˆ– { 0 })))
76simprbi 495 . . . . . . 7 (𝑅 ∈ DivRing β†’ (Unitβ€˜π‘…) = (𝐡 βˆ– { 0 }))
87adantl 480 . . . . . 6 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) β†’ (Unitβ€˜π‘…) = (𝐡 βˆ– { 0 }))
98oveq2d 7442 . . . . 5 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) β†’ (𝑀 β†Ύs (Unitβ€˜π‘…)) = (𝑀 β†Ύs (𝐡 βˆ– { 0 })))
109eleq1d 2814 . . . 4 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) β†’ ((𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp ↔ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))
1110pm5.32i 573 . . 3 (((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) ∧ (𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp) ↔ ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) ∧ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))
12 df-3an 1086 . . 3 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp) ↔ ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) ∧ (𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp))
13 df-3an 1086 . . 3 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp) ↔ ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) ∧ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))
1411, 12, 133bitr4i 302 . 2 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp) ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))
153, 14bitri 274 1 (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   βˆ– cdif 3946  {csn 4632  β€˜cfv 6553  (class class class)co 7426  Basecbs 17187   β†Ύs cress 17216  0gc0g 17428  mulGrpcmgp 20081  Ringcrg 20180  Unitcui 20301  DivRingcdr 20631  TopGrpctgp 23995  TopRingctrg 24080  TopDRingctdrg 24081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-ov 7429  df-drng 20633  df-tdrg 24085
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator