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 ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ( ringLMod ‘ 𝑅 ) ∈ Ban )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → 𝑅 ∈ CMetSp )
2 cmsms ⊢ ( 𝑅 ∈ CMetSp → 𝑅 ∈ MetSp )
3 mstps ⊢ ( 𝑅 ∈ MetSp → 𝑅 ∈ TopSp )
4 1 2 3 3syl ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → 𝑅 ∈ TopSp )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
7 5 6 tpsuni ⊢ ( 𝑅 ∈ TopSp → ( Base ‘ 𝑅 ) = ∪ ( TopOpen ‘ 𝑅 ) )
8 4 7 syl ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ( Base ‘ 𝑅 ) = ∪ ( TopOpen ‘ 𝑅 ) )
9 6 tpstop ⊢ ( 𝑅 ∈ TopSp → ( TopOpen ‘ 𝑅 ) ∈ Top )
10 eqid ⊢ ∪ ( TopOpen ‘ 𝑅 ) = ∪ ( TopOpen ‘ 𝑅 )
11 10 topcld ⊢ ( ( TopOpen ‘ 𝑅 ) ∈ Top → ∪ ( TopOpen ‘ 𝑅 ) ∈ ( Clsd ‘ ( TopOpen ‘ 𝑅 ) ) )
12 4 9 11 3syl ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ∪ ( TopOpen ‘ 𝑅 ) ∈ ( Clsd ‘ ( TopOpen ‘ 𝑅 ) ) )
13 8 12 eqeltrd ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ( Base ‘ 𝑅 ) ∈ ( Clsd ‘ ( TopOpen ‘ 𝑅 ) ) )
14 5 ressid ⊢ ( 𝑅 ∈ NrmRing → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 )
15 14 3ad2ant1 ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 )
16 simp2 ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → 𝑅 ∈ DivRing )
17 15 16 eqeltrd ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ∈ DivRing )
18 simp1 ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → 𝑅 ∈ NrmRing )
19 nrgring ⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ Ring )
20 19 3ad2ant1 ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → 𝑅 ∈ Ring )
21 5 subrgid ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
22 20 21 syl ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
23 rlmval ⊢ ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
24 23 6 srabn ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ CMetSp ∧ ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) ) → ( ( ringLMod ‘ 𝑅 ) ∈ Ban ↔ ( ( Base ‘ 𝑅 ) ∈ ( Clsd ‘ ( TopOpen ‘ 𝑅 ) ) ∧ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ∈ DivRing ) ) )
25 18 1 22 24 syl3anc ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ( ( ringLMod ‘ 𝑅 ) ∈ Ban ↔ ( ( Base ‘ 𝑅 ) ∈ ( Clsd ‘ ( TopOpen ‘ 𝑅 ) ) ∧ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ∈ DivRing ) ) )
26 13 17 25 mpbir2and ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp ) → ( ringLMod ‘ 𝑅 ) ∈ Ban )