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

Theorem istdrg2 24032
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 2726 . . 3 (Unitβ€˜π‘…) = (Unitβ€˜π‘…)
31, 2istdrg 24020 . 2 (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp))
4 istdrg2.b . . . . . . . . 9 𝐡 = (Baseβ€˜π‘…)
5 istdrg2.z . . . . . . . . 9 0 = (0gβ€˜π‘…)
64, 2, 5isdrng 20588 . . . . . . . 8 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unitβ€˜π‘…) = (𝐡 βˆ– { 0 })))
76simprbi 496 . . . . . . 7 (𝑅 ∈ DivRing β†’ (Unitβ€˜π‘…) = (𝐡 βˆ– { 0 }))
87adantl 481 . . . . . 6 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) β†’ (Unitβ€˜π‘…) = (𝐡 βˆ– { 0 }))
98oveq2d 7420 . . . . 5 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) β†’ (𝑀 β†Ύs (Unitβ€˜π‘…)) = (𝑀 β†Ύs (𝐡 βˆ– { 0 })))
109eleq1d 2812 . . . 4 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing) β†’ ((𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp ↔ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))
1110pm5.32i 574 . . 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 303 . 2 ((𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (Unitβ€˜π‘…)) ∈ TopGrp) ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))
153, 14bitri 275 1 (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 β†Ύs (𝐡 βˆ– { 0 })) ∈ TopGrp))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   βˆ– cdif 3940  {csn 4623  β€˜cfv 6536  (class class class)co 7404  Basecbs 17150   β†Ύs cress 17179  0gc0g 17391  mulGrpcmgp 20036  Ringcrg 20135  Unitcui 20254  DivRingcdr 20584  TopGrpctgp 23925  TopRingctrg 24010  TopDRingctdrg 24011
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 2697
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407  df-drng 20586  df-tdrg 24015
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator