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

Metamath Proof Explorer

Theorem csslss

Description: A closed subspace of a pre-Hilbert space is a linear subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses csslss.c 
|- C = ( ClSubSp ` W )
csslss.l 
|- L = ( LSubSp ` W )
Assertion csslss 
|- ( ( W e. PreHil /\ S e. C ) -> S e. L )

Proof

Step Hyp Ref Expression
1 csslss.c 
 |-  C = ( ClSubSp ` W )
2 csslss.l 
 |-  L = ( LSubSp ` W )
3 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
4 3 1 cssi 
 |-  ( S e. C -> S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) )
5 4 adantl 
 |-  ( ( W e. PreHil /\ S e. C ) -> S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 6 3 ocvss 
 |-  ( ( ocv ` W ) ` S ) C_ ( Base ` W )
8 7 a1i 
 |-  ( S e. C -> ( ( ocv ` W ) ` S ) C_ ( Base ` W ) )
9 6 3 2 ocvlss 
 |-  ( ( W e. PreHil /\ ( ( ocv ` W ) ` S ) C_ ( Base ` W ) ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) e. L )
10 8 9 sylan2 
 |-  ( ( W e. PreHil /\ S e. C ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) e. L )
11 5 10 eqeltrd 
 |-  ( ( W e. PreHil /\ S e. C ) -> S e. L )