Metamath Proof Explorer

Theorem ishl2

Description: A Hilbert space is a complete subcomplex pre-Hilbert space over RR or CC . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses hlress.f 
|- F = ( Scalar ` W )
hlress.k 
|- K = ( Base ` F )
Assertion ishl2 
|- ( W e. CHil <-> ( W e. CMetSp /\ W e. CPreHil /\ K e. { RR , CC } ) )

Proof

Step Hyp Ref Expression
1 hlress.f 
 |-  F = ( Scalar ` W )
2 hlress.k 
 |-  K = ( Base ` F )
3 ishl 
 |-  ( W e. CHil <-> ( W e. Ban /\ W e. CPreHil ) )
4 df-3an 
 |-  ( ( W e. CMetSp /\ K e. { RR , CC } /\ W e. CPreHil ) <-> ( ( W e. CMetSp /\ K e. { RR , CC } ) /\ W e. CPreHil ) )
5 3ancomb 
 |-  ( ( W e. CMetSp /\ W e. CPreHil /\ K e. { RR , CC } ) <-> ( W e. CMetSp /\ K e. { RR , CC } /\ W e. CPreHil ) )
6 cphnvc 
 |-  ( W e. CPreHil -> W e. NrmVec )
7 1 isbn 
 |-  ( W e. Ban <-> ( W e. NrmVec /\ W e. CMetSp /\ F e. CMetSp ) )
8 3anass 
 |-  ( ( W e. NrmVec /\ W e. CMetSp /\ F e. CMetSp ) <-> ( W e. NrmVec /\ ( W e. CMetSp /\ F e. CMetSp ) ) )
9 7 8 bitri 
 |-  ( W e. Ban <-> ( W e. NrmVec /\ ( W e. CMetSp /\ F e. CMetSp ) ) )
10 9 baib 
 |-  ( W e. NrmVec -> ( W e. Ban <-> ( W e. CMetSp /\ F e. CMetSp ) ) )
11 6 10 syl 
 |-  ( W e. CPreHil -> ( W e. Ban <-> ( W e. CMetSp /\ F e. CMetSp ) ) )
12 1 2 cphsca 
 |-  ( W e. CPreHil -> F = ( CCfld |`s K ) )
13 12 eleq1d 
 |-  ( W e. CPreHil -> ( F e. CMetSp <-> ( CCfld |`s K ) e. CMetSp ) )
14 1 2 cphsubrg 
 |-  ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )
15 cphlvec 
 |-  ( W e. CPreHil -> W e. LVec )
16 1 lvecdrng 
 |-  ( W e. LVec -> F e. DivRing )
17 15 16 syl 
 |-  ( W e. CPreHil -> F e. DivRing )
18 12 17 eqeltrrd 
 |-  ( W e. CPreHil -> ( CCfld |`s K ) e. DivRing )
19 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
20 19 cncdrg 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ ( CCfld |`s K ) e. DivRing /\ ( CCfld |`s K ) e. CMetSp ) -> K e. { RR , CC } )
21 20 3expia 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ ( CCfld |`s K ) e. DivRing ) -> ( ( CCfld |`s K ) e. CMetSp -> K e. { RR , CC } ) )
22 14 18 21 syl2anc 
 |-  ( W e. CPreHil -> ( ( CCfld |`s K ) e. CMetSp -> K e. { RR , CC } ) )
23 elpri 
 |-  ( K e. { RR , CC } -> ( K = RR \/ K = CC ) )
24 oveq2 
 |-  ( K = RR -> ( CCfld |`s K ) = ( CCfld |`s RR ) )
25 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
26 25 recld2 
 |-  RR e. ( Clsd ` ( TopOpen ` CCfld ) )
27 cncms 
 |-  CCfld e. CMetSp
28 ax-resscn 
 |-  RR C_ CC
29 eqid 
 |-  ( CCfld |`s RR ) = ( CCfld |`s RR )
30 cnfldbas 
 |-  CC = ( Base ` CCfld )
31 29 30 25 cmsss 
 |-  ( ( CCfld e. CMetSp /\ RR C_ CC ) -> ( ( CCfld |`s RR ) e. CMetSp <-> RR e. ( Clsd ` ( TopOpen ` CCfld ) ) ) )
32 27 28 31 mp2an 
 |-  ( ( CCfld |`s RR ) e. CMetSp <-> RR e. ( Clsd ` ( TopOpen ` CCfld ) ) )
33 26 32 mpbir 
 |-  ( CCfld |`s RR ) e. CMetSp
34 24 33 eqeltrdi 
 |-  ( K = RR -> ( CCfld |`s K ) e. CMetSp )
35 oveq2 
 |-  ( K = CC -> ( CCfld |`s K ) = ( CCfld |`s CC ) )
36 30 ressid 
 |-  ( CCfld e. CMetSp -> ( CCfld |`s CC ) = CCfld )
37 27 36 ax-mp 
 |-  ( CCfld |`s CC ) = CCfld
38 37 27 eqeltri 
 |-  ( CCfld |`s CC ) e. CMetSp
39 35 38 eqeltrdi 
 |-  ( K = CC -> ( CCfld |`s K ) e. CMetSp )
40 34 39 jaoi 
 |-  ( ( K = RR \/ K = CC ) -> ( CCfld |`s K ) e. CMetSp )
41 23 40 syl 
 |-  ( K e. { RR , CC } -> ( CCfld |`s K ) e. CMetSp )
42 22 41 impbid1 
 |-  ( W e. CPreHil -> ( ( CCfld |`s K ) e. CMetSp <-> K e. { RR , CC } ) )
43 13 42 bitrd 
 |-  ( W e. CPreHil -> ( F e. CMetSp <-> K e. { RR , CC } ) )
44 43 anbi2d 
 |-  ( W e. CPreHil -> ( ( W e. CMetSp /\ F e. CMetSp ) <-> ( W e. CMetSp /\ K e. { RR , CC } ) ) )
45 11 44 bitrd 
 |-  ( W e. CPreHil -> ( W e. Ban <-> ( W e. CMetSp /\ K e. { RR , CC } ) ) )
46 45 pm5.32ri 
 |-  ( ( W e. Ban /\ W e. CPreHil ) <-> ( ( W e. CMetSp /\ K e. { RR , CC } ) /\ W e. CPreHil ) )
47 4 5 46 3bitr4ri 
 |-  ( ( W e. Ban /\ W e. CPreHil ) <-> ( W e. CMetSp /\ W e. CPreHil /\ K e. { RR , CC } ) )
48 3 47 bitri 
 |-  ( W e. CHil <-> ( W e. CMetSp /\ W e. CPreHil /\ K e. { RR , CC } ) )