Metamath Proof Explorer

Theorem srabn

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

Ref Expression
Hypotheses srabn.a ⊢ A = subringAlg ⁡ W ⁡ S
srabn.j ⊢ J = TopOpen ⁡ W
Assertion srabn ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → A ∈ Ban ↔ S ∈ Clsd ⁡ J ∧ W ↾ 𝑠 S ∈ DivRing

Proof

Step Hyp Ref Expression
1 srabn.a ⊢ A = subringAlg ⁡ W ⁡ S
2 srabn.j ⊢ J = TopOpen ⁡ W
3 simp2 ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → W ∈ CMetSp
4 eqidd ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → Base W = Base W
5 1 a1i ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → A = subringAlg ⁡ W ⁡ S
6 eqid ⊢ Base W = Base W
7 6 subrgss ⊢ S ∈ SubRing ⁡ W → S ⊆ Base W
8 7 3ad2ant3 ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → S ⊆ Base W
9 5 8 srabase ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → Base W = Base A
10 5 8 srads ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → dist ⁡ W = dist ⁡ A
11 10 reseq1d ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → dist ⁡ W ↾ Base W × Base W = dist ⁡ A ↾ Base W × Base W
12 5 8 sratopn ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → TopOpen ⁡ W = TopOpen ⁡ A
13 4 9 11 12 cmspropd ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → W ∈ CMetSp ↔ A ∈ CMetSp
14 3 13 mpbid ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → A ∈ CMetSp
15 eqid ⊢ Scalar ⁡ A = Scalar ⁡ A
16 15 isbn ⊢ A ∈ Ban ↔ A ∈ NrmVec ∧ A ∈ CMetSp ∧ Scalar ⁡ A ∈ CMetSp
17 3anrot ⊢ A ∈ NrmVec ∧ A ∈ CMetSp ∧ Scalar ⁡ A ∈ CMetSp ↔ A ∈ CMetSp ∧ Scalar ⁡ A ∈ CMetSp ∧ A ∈ NrmVec
18 3anass ⊢ A ∈ CMetSp ∧ Scalar ⁡ A ∈ CMetSp ∧ A ∈ NrmVec ↔ A ∈ CMetSp ∧ Scalar ⁡ A ∈ CMetSp ∧ A ∈ NrmVec
19 16 17 18 3bitri ⊢ A ∈ Ban ↔ A ∈ CMetSp ∧ Scalar ⁡ A ∈ CMetSp ∧ A ∈ NrmVec
20 19 baib ⊢ A ∈ CMetSp → A ∈ Ban ↔ Scalar ⁡ A ∈ CMetSp ∧ A ∈ NrmVec
21 14 20 syl ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → A ∈ Ban ↔ Scalar ⁡ A ∈ CMetSp ∧ A ∈ NrmVec
22 5 8 srasca ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → W ↾ 𝑠 S = Scalar ⁡ A
23 22 eleq1d ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → W ↾ 𝑠 S ∈ CMetSp ↔ Scalar ⁡ A ∈ CMetSp
24 eqid ⊢ W ↾ 𝑠 S = W ↾ 𝑠 S
25 24 6 2 cmsss ⊢ W ∈ CMetSp ∧ S ⊆ Base W → W ↾ 𝑠 S ∈ CMetSp ↔ S ∈ Clsd ⁡ J
26 3 8 25 syl2anc ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → W ↾ 𝑠 S ∈ CMetSp ↔ S ∈ Clsd ⁡ J
27 23 26 bitr3d ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → Scalar ⁡ A ∈ CMetSp ↔ S ∈ Clsd ⁡ J
28 1 sranlm ⊢ W ∈ NrmRing ∧ S ∈ SubRing ⁡ W → A ∈ NrmMod
29 28 3adant2 ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → A ∈ NrmMod
30 15 isnvc2 ⊢ A ∈ NrmVec ↔ A ∈ NrmMod ∧ Scalar ⁡ A ∈ DivRing
31 30 baib ⊢ A ∈ NrmMod → A ∈ NrmVec ↔ Scalar ⁡ A ∈ DivRing
32 29 31 syl ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → A ∈ NrmVec ↔ Scalar ⁡ A ∈ DivRing
33 22 eleq1d ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → W ↾ 𝑠 S ∈ DivRing ↔ Scalar ⁡ A ∈ DivRing
34 32 33 bitr4d ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → A ∈ NrmVec ↔ W ↾ 𝑠 S ∈ DivRing
35 27 34 anbi12d ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → Scalar ⁡ A ∈ CMetSp ∧ A ∈ NrmVec ↔ S ∈ Clsd ⁡ J ∧ W ↾ 𝑠 S ∈ DivRing
36 21 35 bitrd ⊢ W ∈ NrmRing ∧ W ∈ CMetSp ∧ S ∈ SubRing ⁡ W → A ∈ Ban ↔ S ∈ Clsd ⁡ J ∧ W ↾ 𝑠 S ∈ DivRing