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 e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( A e. Ban <-> ( S e. ( Clsd ` J ) /\ ( W |`s S ) e. DivRing ) ) )

Proof

Step Hyp Ref Expression
1 srabn.a 
 |-  A = ( ( subringAlg ` W ) ` S )
2 srabn.j 
 |-  J = ( TopOpen ` W )
3 simp2 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> W e. CMetSp )
4 eqidd 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( Base ` W ) = ( Base ` W ) )
5 1 a1i 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> A = ( ( subringAlg ` W ) ` S ) )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 6 subrgss 
 |-  ( S e. ( SubRing ` W ) -> S C_ ( Base ` W ) )
8 7 3ad2ant3 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> S C_ ( Base ` W ) )
9 5 8 srabase 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( Base ` W ) = ( Base ` A ) )
10 5 8 srads 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( dist ` W ) = ( dist ` A ) )
11 10 reseq1d 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) = ( ( dist ` A ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) )
12 5 8 sratopn 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( TopOpen ` W ) = ( TopOpen ` A ) )
13 4 9 11 12 cmspropd 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( W e. CMetSp <-> A e. CMetSp ) )
14 3 13 mpbid 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> A e. CMetSp )
15 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
16 15 isbn 
 |-  ( A e. Ban <-> ( A e. NrmVec /\ A e. CMetSp /\ ( Scalar ` A ) e. CMetSp ) )
17 3anrot 
 |-  ( ( A e. NrmVec /\ A e. CMetSp /\ ( Scalar ` A ) e. CMetSp ) <-> ( A e. CMetSp /\ ( Scalar ` A ) e. CMetSp /\ A e. NrmVec ) )
18 3anass 
 |-  ( ( A e. CMetSp /\ ( Scalar ` A ) e. CMetSp /\ A e. NrmVec ) <-> ( A e. CMetSp /\ ( ( Scalar ` A ) e. CMetSp /\ A e. NrmVec ) ) )
19 16 17 18 3bitri 
 |-  ( A e. Ban <-> ( A e. CMetSp /\ ( ( Scalar ` A ) e. CMetSp /\ A e. NrmVec ) ) )
20 19 baib 
 |-  ( A e. CMetSp -> ( A e. Ban <-> ( ( Scalar ` A ) e. CMetSp /\ A e. NrmVec ) ) )
21 14 20 syl 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( A e. Ban <-> ( ( Scalar ` A ) e. CMetSp /\ A e. NrmVec ) ) )
22 5 8 srasca 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( W |`s S ) = ( Scalar ` A ) )
23 22 eleq1d 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( ( W |`s S ) e. CMetSp <-> ( Scalar ` A ) e. CMetSp ) )
24 eqid 
 |-  ( W |`s S ) = ( W |`s S )
25 24 6 2 cmsss 
 |-  ( ( W e. CMetSp /\ S C_ ( Base ` W ) ) -> ( ( W |`s S ) e. CMetSp <-> S e. ( Clsd ` J ) ) )
26 3 8 25 syl2anc 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( ( W |`s S ) e. CMetSp <-> S e. ( Clsd ` J ) ) )
27 23 26 bitr3d 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( ( Scalar ` A ) e. CMetSp <-> S e. ( Clsd ` J ) ) )
28 1 sranlm 
 |-  ( ( W e. NrmRing /\ S e. ( SubRing ` W ) ) -> A e. NrmMod )
29 28 3adant2 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> A e. NrmMod )
30 15 isnvc2 
 |-  ( A e. NrmVec <-> ( A e. NrmMod /\ ( Scalar ` A ) e. DivRing ) )
31 30 baib 
 |-  ( A e. NrmMod -> ( A e. NrmVec <-> ( Scalar ` A ) e. DivRing ) )
32 29 31 syl 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( A e. NrmVec <-> ( Scalar ` A ) e. DivRing ) )
33 22 eleq1d 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( ( W |`s S ) e. DivRing <-> ( Scalar ` A ) e. DivRing ) )
34 32 33 bitr4d 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( A e. NrmVec <-> ( W |`s S ) e. DivRing ) )
35 27 34 anbi12d 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( ( ( Scalar ` A ) e. CMetSp /\ A e. NrmVec ) <-> ( S e. ( Clsd ` J ) /\ ( W |`s S ) e. DivRing ) ) )
36 21 35 bitrd 
 |-  ( ( W e. NrmRing /\ W e. CMetSp /\ S e. ( SubRing ` W ) ) -> ( A e. Ban <-> ( S e. ( Clsd ` J ) /\ ( W |`s S ) e. DivRing ) ) )