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

Metamath Proof Explorer

Theorem iscss

Description: The predicate "is a closed subspace" (of a pre-Hilbert space). (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cssval.o 
|- ._|_ = ( ocv ` W )
cssval.c 
|- C = ( ClSubSp ` W )
Assertion iscss 
|- ( W e. X -> ( S e. C <-> S = ( ._|_ ` ( ._|_ ` S ) ) ) )

Proof

Step Hyp Ref Expression
1 cssval.o 
 |-  ._|_ = ( ocv ` W )
2 cssval.c 
 |-  C = ( ClSubSp ` W )
3 1 2 cssval 
 |-  ( W e. X -> C = { s | s = ( ._|_ ` ( ._|_ ` s ) ) } )
4 3 eleq2d 
 |-  ( W e. X -> ( S e. C <-> S e. { s | s = ( ._|_ ` ( ._|_ ` s ) ) } ) )
5 id 
 |-  ( S = ( ._|_ ` ( ._|_ ` S ) ) -> S = ( ._|_ ` ( ._|_ ` S ) ) )
6 fvex 
 |-  ( ._|_ ` ( ._|_ ` S ) ) e. _V
7 5 6 eqeltrdi 
 |-  ( S = ( ._|_ ` ( ._|_ ` S ) ) -> S e. _V )
8 id 
 |-  ( s = S -> s = S )
9 2fveq3 
 |-  ( s = S -> ( ._|_ ` ( ._|_ ` s ) ) = ( ._|_ ` ( ._|_ ` S ) ) )
10 8 9 eqeq12d 
 |-  ( s = S -> ( s = ( ._|_ ` ( ._|_ ` s ) ) <-> S = ( ._|_ ` ( ._|_ ` S ) ) ) )
11 7 10 elab3 
 |-  ( S e. { s | s = ( ._|_ ` ( ._|_ ` s ) ) } <-> S = ( ._|_ ` ( ._|_ ` S ) ) )
12 4 11 bitrdi 
 |-  ( W e. X -> ( S e. C <-> S = ( ._|_ ` ( ._|_ ` S ) ) ) )