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 ⊢ M = mulGrp R
istdrg2.b ⊢ B = Base R
istdrg2.z ⊢ 0 ˙ = 0 R
Assertion istdrg2 ⊢ R ∈ TopDRing ↔ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 B ∖ 0 ˙ ∈ TopGrp

Proof

Step Hyp Ref Expression
1 istdrg2.m ⊢ M = mulGrp R
2 istdrg2.b ⊢ B = Base R
3 istdrg2.z ⊢ 0 ˙ = 0 R
4 eqid ⊢ Unit ⁡ R = Unit ⁡ R
5 1 4 istdrg ⊢ R ∈ TopDRing ↔ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 Unit ⁡ R ∈ TopGrp
6 2 4 3 isdrng ⊢ R ∈ DivRing ↔ R ∈ Ring ∧ Unit ⁡ R = B ∖ 0 ˙
7 6 simprbi ⊢ R ∈ DivRing → Unit ⁡ R = B ∖ 0 ˙
8 7 adantl ⊢ R ∈ TopRing ∧ R ∈ DivRing → Unit ⁡ R = B ∖ 0 ˙
9 8 oveq2d ⊢ R ∈ TopRing ∧ R ∈ DivRing → M ↾ 𝑠 Unit ⁡ R = M ↾ 𝑠 B ∖ 0 ˙
10 9 eleq1d ⊢ R ∈ TopRing ∧ R ∈ DivRing → M ↾ 𝑠 Unit ⁡ R ∈ TopGrp ↔ M ↾ 𝑠 B ∖ 0 ˙ ∈ TopGrp
11 10 pm5.32i ⊢ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 Unit ⁡ R ∈ TopGrp ↔ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 B ∖ 0 ˙ ∈ TopGrp
12 df-3an ⊢ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 Unit ⁡ R ∈ TopGrp ↔ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 Unit ⁡ R ∈ TopGrp
13 df-3an ⊢ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 B ∖ 0 ˙ ∈ TopGrp ↔ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 B ∖ 0 ˙ ∈ TopGrp
14 11 12 13 3bitr4i ⊢ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 Unit ⁡ R ∈ TopGrp ↔ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 B ∖ 0 ˙ ∈ TopGrp
15 5 14 bitri ⊢ R ∈ TopDRing ↔ R ∈ TopRing ∧ R ∈ DivRing ∧ M ↾ 𝑠 B ∖ 0 ˙ ∈ TopGrp