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 e. NrmRing /\ R e. DivRing ) -> R e. TopDRing )

Proof

Step Hyp Ref Expression
1 nrgtrg 
 |-  ( R e. NrmRing -> R e. TopRing )
2 1 adantr 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> R e. TopRing )
3 simpr 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> R e. DivRing )
4 nrgring 
 |-  ( R e. NrmRing -> R e. Ring )
5 4 adantr 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> R e. Ring )
6 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
7 eqid 
 |-  ( ( mulGrp ` R ) |`s ( Unit ` R ) ) = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
8 6 7 unitgrp 
 |-  ( R e. Ring -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. Grp )
9 5 8 syl 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. Grp )
10 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
11 10 trgtmd 
 |-  ( R e. TopRing -> ( mulGrp ` R ) e. TopMnd )
12 2 11 syl 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> ( mulGrp ` R ) e. TopMnd )
13 6 10 unitsubm 
 |-  ( R e. Ring -> ( Unit ` R ) e. ( SubMnd ` ( mulGrp ` R ) ) )
14 5 13 syl 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> ( Unit ` R ) e. ( SubMnd ` ( mulGrp ` R ) ) )
15 7 submtmd 
 |-  ( ( ( mulGrp ` R ) e. TopMnd /\ ( Unit ` R ) e. ( SubMnd ` ( mulGrp ` R ) ) ) -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. TopMnd )
16 12 14 15 syl2anc 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. TopMnd )
17 eqid 
 |-  ( Base ` R ) = ( Base ` R )
18 eqid 
 |-  ( invr ` R ) = ( invr ` R )
19 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
20 17 6 18 19 nrginvrcn 
 |-  ( R e. NrmRing -> ( invr ` R ) e. ( ( ( TopOpen ` R ) |`t ( Unit ` R ) ) Cn ( ( TopOpen ` R ) |`t ( Unit ` R ) ) ) )
21 20 adantr 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> ( invr ` R ) e. ( ( ( TopOpen ` R ) |`t ( Unit ` R ) ) Cn ( ( TopOpen ` R ) |`t ( Unit ` R ) ) ) )
22 10 19 mgptopn 
 |-  ( TopOpen ` R ) = ( TopOpen ` ( mulGrp ` R ) )
23 7 22 resstopn 
 |-  ( ( TopOpen ` R ) |`t ( Unit ` R ) ) = ( TopOpen ` ( ( mulGrp ` R ) |`s ( Unit ` R ) ) )
24 6 7 18 invrfval 
 |-  ( invr ` R ) = ( invg ` ( ( mulGrp ` R ) |`s ( Unit ` R ) ) )
25 23 24 istgp 
 |-  ( ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. TopGrp <-> ( ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. Grp /\ ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. TopMnd /\ ( invr ` R ) e. ( ( ( TopOpen ` R ) |`t ( Unit ` R ) ) Cn ( ( TopOpen ` R ) |`t ( Unit ` R ) ) ) ) )
26 9 16 21 25 syl3anbrc 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. TopGrp )
27 10 6 istdrg 
 |-  ( R e. TopDRing <-> ( R e. TopRing /\ R e. DivRing /\ ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. TopGrp ) )
28 2 3 26 27 syl3anbrc 
 |-  ( ( R e. NrmRing /\ R e. DivRing ) -> R e. TopDRing )