Metamath Proof Explorer

Theorem nrgtrg

Description: A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015) (Proof shortened by AV, 31-Oct-2024)

Ref Expression
Assertion nrgtrg 
|- ( R e. NrmRing -> R e. TopRing )

Proof

Step Hyp Ref Expression
1 nrgtgp 
 |-  ( R e. NrmRing -> R e. TopGrp )
2 nrgring 
 |-  ( R e. NrmRing -> R e. Ring )
3 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
4 3 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
5 2 4 syl 
 |-  ( R e. NrmRing -> ( mulGrp ` R ) e. Mnd )
6 tgptps 
 |-  ( R e. TopGrp -> R e. TopSp )
7 1 6 syl 
 |-  ( R e. NrmRing -> R e. TopSp )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
10 8 9 istps 
 |-  ( R e. TopSp <-> ( TopOpen ` R ) e. ( TopOn ` ( Base ` R ) ) )
11 7 10 sylib 
 |-  ( R e. NrmRing -> ( TopOpen ` R ) e. ( TopOn ` ( Base ` R ) ) )
12 3 8 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
13 3 9 mgptopn 
 |-  ( TopOpen ` R ) = ( TopOpen ` ( mulGrp ` R ) )
14 12 13 istps 
 |-  ( ( mulGrp ` R ) e. TopSp <-> ( TopOpen ` R ) e. ( TopOn ` ( Base ` R ) ) )
15 11 14 sylibr 
 |-  ( R e. NrmRing -> ( mulGrp ` R ) e. TopSp )
16 rlmnlm 
 |-  ( R e. NrmRing -> ( ringLMod ` R ) e. NrmMod )
17 rlmsca2 
 |-  ( _I ` R ) = ( Scalar ` ( ringLMod ` R ) )
18 rlmscaf 
 |-  ( +f ` ( mulGrp ` R ) ) = ( .sf ` ( ringLMod ` R ) )
19 rlmtopn 
 |-  ( TopOpen ` R ) = ( TopOpen ` ( ringLMod ` R ) )
20 baseid 
 |-  Base = Slot ( Base ` ndx )
21 20 8 strfvi 
 |-  ( Base ` R ) = ( Base ` ( _I ` R ) )
22 21 a1i 
 |-  ( T. -> ( Base ` R ) = ( Base ` ( _I ` R ) ) )
23 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
24 eqid 
 |-  ( TopSet ` R ) = ( TopSet ` R )
25 23 24 strfvi 
 |-  ( TopSet ` R ) = ( TopSet ` ( _I ` R ) )
26 25 a1i 
 |-  ( T. -> ( TopSet ` R ) = ( TopSet ` ( _I ` R ) ) )
27 22 26 topnpropd 
 |-  ( T. -> ( TopOpen ` R ) = ( TopOpen ` ( _I ` R ) ) )
28 27 mptru 
 |-  ( TopOpen ` R ) = ( TopOpen ` ( _I ` R ) )
29 17 18 19 28 nlmvscn 
 |-  ( ( ringLMod ` R ) e. NrmMod -> ( +f ` ( mulGrp ` R ) ) e. ( ( ( TopOpen ` R ) tX ( TopOpen ` R ) ) Cn ( TopOpen ` R ) ) )
30 16 29 syl 
 |-  ( R e. NrmRing -> ( +f ` ( mulGrp ` R ) ) e. ( ( ( TopOpen ` R ) tX ( TopOpen ` R ) ) Cn ( TopOpen ` R ) ) )
31 eqid 
 |-  ( +f ` ( mulGrp ` R ) ) = ( +f ` ( mulGrp ` R ) )
32 31 13 istmd 
 |-  ( ( mulGrp ` R ) e. TopMnd <-> ( ( mulGrp ` R ) e. Mnd /\ ( mulGrp ` R ) e. TopSp /\ ( +f ` ( mulGrp ` R ) ) e. ( ( ( TopOpen ` R ) tX ( TopOpen ` R ) ) Cn ( TopOpen ` R ) ) ) )
33 5 15 30 32 syl3anbrc 
 |-  ( R e. NrmRing -> ( mulGrp ` R ) e. TopMnd )
34 3 istrg 
 |-  ( R e. TopRing <-> ( R e. TopGrp /\ R e. Ring /\ ( mulGrp ` R ) e. TopMnd ) )
35 1 2 33 34 syl3anbrc 
 |-  ( R e. NrmRing -> R e. TopRing )