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	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	istdrg2	$⊢ R \in TopDRing \leftrightarrow (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in TopGrp)$

Proof

Step	Hyp	Ref	Expression
1		istdrg2.m	$⊢ M = {mulGrp}_{R}$
2		istdrg2.b	$⊢ B = {Base}_{R}$
3		istdrg2.z	$⊢ \underset{˙}{0} = 0_{R}$
4		eqid	$⊢ Unit (R) = Unit (R)$
5	1 4	istdrg	$⊢ R \in TopDRing \leftrightarrow (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} Unit (R) \in TopGrp)$
6	2 4 3	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\})$
7	6	simprbi	$⊢ R \in DivRing \to Unit (R) = B ∖ \{\underset{˙}{0}\}$
8	7	adantl	$⊢ (R \in TopRing \land R \in DivRing) \to Unit (R) = B ∖ \{\underset{˙}{0}\}$
9	8	oveq2d	$⊢ (R \in TopRing \land R \in DivRing) \to M ↾_{𝑠} Unit (R) = M ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
10	9	eleq1d	$⊢ (R \in TopRing \land R \in DivRing) \to (M ↾_{𝑠} Unit (R) \in TopGrp \leftrightarrow M ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in TopGrp)$
11	10	pm5.32i	$⊢ ((R \in TopRing \land R \in DivRing) \land M ↾_{𝑠} Unit (R) \in TopGrp) \leftrightarrow ((R \in TopRing \land R \in DivRing) \land M ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in TopGrp)$
12		df-3an	$⊢ (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} Unit (R) \in TopGrp) \leftrightarrow ((R \in TopRing \land R \in DivRing) \land M ↾_{𝑠} Unit (R) \in TopGrp)$
13		df-3an	$⊢ (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in TopGrp) \leftrightarrow ((R \in TopRing \land R \in DivRing) \land M ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in TopGrp)$
14	11 12 13	3bitr4i	$⊢ (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} Unit (R) \in TopGrp) \leftrightarrow (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in TopGrp)$
15	5 14	bitri	$⊢ R \in TopDRing \leftrightarrow (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in TopGrp)$