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 )