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 ∈ NrmRing ∧ R ∈ DivRing ∧ R ∈ CMetSp → ringLMod ⁡ R ∈ Ban

Proof

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