This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chlcsschl

Description: A closed subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 10-Apr-2008) (Revised by AV, 8-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 cmslsschl.x 
 |-  X = ( W |`s U )
2 chlcsschl.s 
 |-  S = ( ClSubSp ` W )
3 hlbn 
 |-  ( W e. CHil -> W e. Ban )
4 hlcph 
 |-  ( W e. CHil -> W e. CPreHil )
5 3 4 jca 
 |-  ( W e. CHil -> ( W e. Ban /\ W e. CPreHil ) )
6 1 2 bncssbn 
 |-  ( ( ( W e. Ban /\ W e. CPreHil ) /\ U e. S ) -> X e. Ban )
7 5 6 sylan 
 |-  ( ( W e. CHil /\ U e. S ) -> X e. Ban )
8 hlphl 
 |-  ( W e. CHil -> W e. PreHil )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 2 9 csslss 
 |-  ( ( W e. PreHil /\ U e. S ) -> U e. ( LSubSp ` W ) )
11 8 10 sylan 
 |-  ( ( W e. CHil /\ U e. S ) -> U e. ( LSubSp ` W ) )
12 1 9 cphsscph 
 |-  ( ( W e. CPreHil /\ U e. ( LSubSp ` W ) ) -> X e. CPreHil )
13 4 11 12 syl2an2r 
 |-  ( ( W e. CHil /\ U e. S ) -> X e. CPreHil )
14 ishl 
 |-  ( X e. CHil <-> ( X e. Ban /\ X e. CPreHil ) )
15 7 13 14 sylanbrc 
 |-  ( ( W e. CHil /\ U e. S ) -> X e. CHil )