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 ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
srabn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion srabn ( ( 𝑊 ∈ NrmRing ∧ 𝑊 ∈ CMetSp ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝐴 ∈ Ban ↔ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑊 ↾s 𝑆 ) ∈ DivRing ) ) )

Proof

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