nrgtdrg

Description: A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015)

		Ref	Expression
	Assertion	nrgtdrg	$⊢ (R \in NrmRing \land R \in DivRing) \to R \in TopDRing$

Proof

Step	Hyp	Ref	Expression
1		nrgtrg	$⊢ R \in NrmRing \to R \in TopRing$
2	1	adantr	$⊢ (R \in NrmRing \land R \in DivRing) \to R \in TopRing$
3		simpr	$⊢ (R \in NrmRing \land R \in DivRing) \to R \in DivRing$
4		nrgring	$⊢ R \in NrmRing \to R \in Ring$
5	4	adantr	$⊢ (R \in NrmRing \land R \in DivRing) \to R \in Ring$
6		eqid	$⊢ Unit (R) = Unit (R)$
7		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
8	6 7	unitgrp	$⊢ R \in Ring \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in Grp$
9	5 8	syl	$⊢ (R \in NrmRing \land R \in DivRing) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in Grp$
10		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
11	10	trgtmd	$⊢ R \in TopRing \to {mulGrp}_{R} \in TopMnd$
12	2 11	syl	$⊢ (R \in NrmRing \land R \in DivRing) \to {mulGrp}_{R} \in TopMnd$
13	6 10	unitsubm	$⊢ R \in Ring \to Unit (R) \in SubMnd ({mulGrp}_{R})$
14	5 13	syl	$⊢ (R \in NrmRing \land R \in DivRing) \to Unit (R) \in SubMnd ({mulGrp}_{R})$
15	7	submtmd	$⊢ ({mulGrp}_{R} \in TopMnd \land Unit (R) \in SubMnd ({mulGrp}_{R})) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in TopMnd$
16	12 14 15	syl2anc	$⊢ (R \in NrmRing \land R \in DivRing) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in TopMnd$
17		eqid	$⊢ {Base}_{R} = {Base}_{R}$
18		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
19		eqid	$⊢ TopOpen (R) = TopOpen (R)$
20	17 6 18 19	nrginvrcn	$⊢ R \in NrmRing \to {inv}_{r} (R) \in ((TopOpen (R) ↾_{𝑡} Unit (R)) Cn (TopOpen (R) ↾_{𝑡} Unit (R)))$
21	20	adantr	$⊢ (R \in NrmRing \land R \in DivRing) \to {inv}_{r} (R) \in ((TopOpen (R) ↾_{𝑡} Unit (R)) Cn (TopOpen (R) ↾_{𝑡} Unit (R)))$
22	10 19	mgptopn	$⊢ TopOpen (R) = TopOpen ({mulGrp}_{R})$
23	7 22	resstopn	$⊢ TopOpen (R) ↾_{𝑡} Unit (R) = TopOpen ({mulGrp}_{R} ↾_{𝑠} Unit (R))$
24	6 7 18	invrfval	$⊢ {inv}_{r} (R) = {inv}_{g} ({mulGrp}_{R} ↾_{𝑠} Unit (R))$
25	23 24	istgp	$⊢ {mulGrp}_{R} ↾_{𝑠} Unit (R) \in TopGrp \leftrightarrow ({mulGrp}_{R} ↾_{𝑠} Unit (R) \in Grp \land {mulGrp}_{R} ↾_{𝑠} Unit (R) \in TopMnd \land {inv}_{r} (R) \in ((TopOpen (R) ↾_{𝑡} Unit (R)) Cn (TopOpen (R) ↾_{𝑡} Unit (R))))$
26	9 16 21 25	syl3anbrc	$⊢ (R \in NrmRing \land R \in DivRing) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in TopGrp$
27	10 6	istdrg	$⊢ R \in TopDRing \leftrightarrow (R \in TopRing \land R \in DivRing \land {mulGrp}_{R} ↾_{𝑠} Unit (R) \in TopGrp)$
28	2 3 26 27	syl3anbrc	$⊢ (R \in NrmRing \land R \in DivRing) \to R \in TopDRing$

Metamath Proof Explorer

Theorem nrgtdrg

Proof