Metamath Proof Explorer

Theorem rlmbn

Description: The ring module over a complete normed division ring is a Banach space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion rlmbn 
|- ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> ( ringLMod ` R ) e. Ban )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> R e. CMetSp )
2 cmsms 
 |-  ( R e. CMetSp -> R e. MetSp )
3 mstps 
 |-  ( R e. MetSp -> R e. TopSp )
4 1 2 3 3syl 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> R e. TopSp )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
7 5 6 tpsuni 
 |-  ( R e. TopSp -> ( Base ` R ) = U. ( TopOpen ` R ) )
8 4 7 syl 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> ( Base ` R ) = U. ( TopOpen ` R ) )
9 6 tpstop 
 |-  ( R e. TopSp -> ( TopOpen ` R ) e. Top )
10 eqid 
 |-  U. ( TopOpen ` R ) = U. ( TopOpen ` R )
11 10 topcld 
 |-  ( ( TopOpen ` R ) e. Top -> U. ( TopOpen ` R ) e. ( Clsd ` ( TopOpen ` R ) ) )
12 4 9 11 3syl 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> U. ( TopOpen ` R ) e. ( Clsd ` ( TopOpen ` R ) ) )
13 8 12 eqeltrd 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> ( Base ` R ) e. ( Clsd ` ( TopOpen ` R ) ) )
14 5 ressid 
 |-  ( R e. NrmRing -> ( R |`s ( Base ` R ) ) = R )
15 14 3ad2ant1 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> ( R |`s ( Base ` R ) ) = R )
16 simp2 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> R e. DivRing )
17 15 16 eqeltrd 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> ( R |`s ( Base ` R ) ) e. DivRing )
18 simp1 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> R e. NrmRing )
19 nrgring 
 |-  ( R e. NrmRing -> R e. Ring )
20 19 3ad2ant1 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> R e. Ring )
21 5 subrgid 
 |-  ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
22 20 21 syl 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> ( Base ` R ) e. ( SubRing ` R ) )
23 rlmval 
 |-  ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
24 23 6 srabn 
 |-  ( ( R e. NrmRing /\ R e. CMetSp /\ ( Base ` R ) e. ( SubRing ` R ) ) -> ( ( ringLMod ` R ) e. Ban <-> ( ( Base ` R ) e. ( Clsd ` ( TopOpen ` R ) ) /\ ( R |`s ( Base ` R ) ) e. DivRing ) ) )
25 18 1 22 24 syl3anc 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> ( ( ringLMod ` R ) e. Ban <-> ( ( Base ` R ) e. ( Clsd ` ( TopOpen ` R ) ) /\ ( R |`s ( Base ` R ) ) e. DivRing ) ) )
26 13 17 25 mpbir2and 
 |-  ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> ( ringLMod ` R ) e. Ban )