Metamath Proof Explorer

Theorem cmslsschl

Description: A complete linear subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by AV, 8-Oct-2022)

Ref Expression
Hypotheses cmslsschl.x 
|- X = ( W |`s U )
cmslsschl.s 
|- S = ( LSubSp ` W )
Assertion cmslsschl 
|- ( ( W e. CHil /\ X e. CMetSp /\ U e. S ) -> X e. CHil )

Proof

Step Hyp Ref Expression
1 cmslsschl.x 
 |-  X = ( W |`s U )
2 cmslsschl.s 
 |-  S = ( LSubSp ` W )
3 hlbn 
 |-  ( W e. CHil -> W e. Ban )
4 bnnvc 
 |-  ( W e. Ban -> W e. NrmVec )
5 3 4 syl 
 |-  ( W e. CHil -> W e. NrmVec )
6 5 3ad2ant1 
 |-  ( ( W e. CHil /\ X e. CMetSp /\ U e. S ) -> W e. NrmVec )
7 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
8 7 bnsca 
 |-  ( W e. Ban -> ( Scalar ` W ) e. CMetSp )
9 3 8 syl 
 |-  ( W e. CHil -> ( Scalar ` W ) e. CMetSp )
10 9 3ad2ant1 
 |-  ( ( W e. CHil /\ X e. CMetSp /\ U e. S ) -> ( Scalar ` W ) e. CMetSp )
11 3simpc 
 |-  ( ( W e. CHil /\ X e. CMetSp /\ U e. S ) -> ( X e. CMetSp /\ U e. S ) )
12 1 2 cmslssbn 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp ) /\ ( X e. CMetSp /\ U e. S ) ) -> X e. Ban )
13 6 10 11 12 syl21anc 
 |-  ( ( W e. CHil /\ X e. CMetSp /\ U e. S ) -> X e. Ban )
14 hlcph 
 |-  ( W e. CHil -> W e. CPreHil )
15 1 2 cphsscph 
 |-  ( ( W e. CPreHil /\ U e. S ) -> X e. CPreHil )
16 14 15 sylan 
 |-  ( ( W e. CHil /\ U e. S ) -> X e. CPreHil )
17 16 3adant2 
 |-  ( ( W e. CHil /\ X e. CMetSp /\ U e. S ) -> X e. CPreHil )
18 ishl 
 |-  ( X e. CHil <-> ( X e. Ban /\ X e. CPreHil ) )
19 13 17 18 sylanbrc 
 |-  ( ( W e. CHil /\ X e. CMetSp /\ U e. S ) -> X e. CHil )