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 ) )