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

Metamath Proof Explorer

Theorem ocvcss

Description: The orthocomplement of any set is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cssss.v 
|- V = ( Base ` W )
cssss.c 
|- C = ( ClSubSp ` W )
ocvcss.o 
|- ._|_ = ( ocv ` W )
Assertion ocvcss 
|- ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) e. C )

Proof

Step Hyp Ref Expression
1 cssss.v 
 |-  V = ( Base ` W )
2 cssss.c 
 |-  C = ( ClSubSp ` W )
3 ocvcss.o 
 |-  ._|_ = ( ocv ` W )
4 1 3 ocvocv 
 |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )
5 3 ocv2ss 
 |-  ( S C_ ( ._|_ ` ( ._|_ ` S ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) C_ ( ._|_ ` S ) )
6 4 5 syl 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) C_ ( ._|_ ` S ) )
7 1 3 ocvss 
 |-  ( ._|_ ` S ) C_ V
8 7 a1i 
 |-  ( S C_ V -> ( ._|_ ` S ) C_ V )
9 1 2 3 iscss2 
 |-  ( ( W e. PreHil /\ ( ._|_ ` S ) C_ V ) -> ( ( ._|_ ` S ) e. C <-> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) C_ ( ._|_ ` S ) ) )
10 8 9 sylan2 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ( ._|_ ` S ) e. C <-> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) C_ ( ._|_ ` S ) ) )
11 6 10 mpbird 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) e. C )