Metamath Proof Explorer


Theorem nrgtdrg

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

Ref Expression
Assertion nrgtdrg R NrmRing R DivRing R TopDRing

Proof

Step Hyp Ref Expression
1 nrgtrg R NrmRing R TopRing
2 1 adantr R NrmRing R DivRing R TopRing
3 simpr R NrmRing R DivRing R DivRing
4 nrgring R NrmRing R Ring
5 4 adantr R NrmRing R DivRing R Ring
6 eqid Unit R = Unit R
7 eqid mulGrp R 𝑠 Unit R = mulGrp R 𝑠 Unit R
8 6 7 unitgrp R Ring mulGrp R 𝑠 Unit R Grp
9 5 8 syl R NrmRing R DivRing mulGrp R 𝑠 Unit R Grp
10 eqid mulGrp R = mulGrp R
11 10 trgtmd R TopRing mulGrp R TopMnd
12 2 11 syl R NrmRing R DivRing mulGrp R TopMnd
13 6 10 unitsubm R Ring Unit R SubMnd mulGrp R
14 5 13 syl R NrmRing R DivRing Unit R SubMnd mulGrp R
15 7 submtmd mulGrp R TopMnd Unit R SubMnd mulGrp R mulGrp R 𝑠 Unit R TopMnd
16 12 14 15 syl2anc R NrmRing R DivRing mulGrp R 𝑠 Unit R 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 NrmRing inv r R TopOpen R 𝑡 Unit R Cn TopOpen R 𝑡 Unit R
21 20 adantr R NrmRing R DivRing inv r R 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 TopGrp mulGrp R 𝑠 Unit R Grp mulGrp R 𝑠 Unit R TopMnd inv r R TopOpen R 𝑡 Unit R Cn TopOpen R 𝑡 Unit R
26 9 16 21 25 syl3anbrc R NrmRing R DivRing mulGrp R 𝑠 Unit R TopGrp
27 10 6 istdrg R TopDRing R TopRing R DivRing mulGrp R 𝑠 Unit R TopGrp
28 2 3 26 27 syl3anbrc R NrmRing R DivRing R TopDRing