This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem istdrg2

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)

Ref Expression
Hypotheses istdrg2.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
istdrg2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
istdrg2.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion istdrg2 ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s ( 𝐵 ∖ { 0 } ) ) ∈ TopGrp ) )

Proof

Step Hyp Ref Expression
1 istdrg2.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2 istdrg2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 istdrg2.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
5 1 4 istdrg ⊢ ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ) )
6 2 4 3 isdrng ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) )
7 6 simprbi ⊢ ( 𝑅 ∈ DivRing → ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) )
8 7 adantl ⊢ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) → ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) )
9 8 oveq2d ⊢ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) → ( 𝑀 ↾s ( Unit ‘ 𝑅 ) ) = ( 𝑀 ↾s ( 𝐵 ∖ { 0 } ) ) )
10 9 eleq1d ⊢ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) → ( ( 𝑀 ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ↔ ( 𝑀 ↾s ( 𝐵 ∖ { 0 } ) ) ∈ TopGrp ) )
11 10 pm5.32i ⊢ ( ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑀 ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ) ↔ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑀 ↾s ( 𝐵 ∖ { 0 } ) ) ∈ TopGrp ) )
12 df-3an ⊢ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ) ↔ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑀 ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ) )
13 df-3an ⊢ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s ( 𝐵 ∖ { 0 } ) ) ∈ TopGrp ) ↔ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑀 ↾s ( 𝐵 ∖ { 0 } ) ) ∈ TopGrp ) )
14 11 12 13 3bitr4i ⊢ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ) ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s ( 𝐵 ∖ { 0 } ) ) ∈ TopGrp ) )
15 5 14 bitri ⊢ ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s ( 𝐵 ∖ { 0 } ) ) ∈ TopGrp ) )