Metamath Proof Explorer


Theorem ocvocv

Description: A set is contained in its double orthocomplement. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ocvss.v
|- V = ( Base ` W )
ocvss.o
|- ._|_ = ( ocv ` W )
Assertion ocvocv
|- ( ( W e. PreHil /\ S C_ V ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )

Proof

Step Hyp Ref Expression
1 ocvss.v
 |-  V = ( Base ` W )
2 ocvss.o
 |-  ._|_ = ( ocv ` W )
3 1 2 ocvss
 |-  ( ._|_ ` S ) C_ V
4 3 a1i
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> ( ._|_ ` S ) C_ V )
5 simpr
 |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ V )
6 5 sselda
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> x e. V )
7 eqid
 |-  ( .i ` W ) = ( .i ` W )
8 eqid
 |-  ( Scalar ` W ) = ( Scalar ` W )
9 eqid
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
10 1 7 8 9 2 ocvi
 |-  ( ( y e. ( ._|_ ` S ) /\ x e. S ) -> ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
11 10 ancoms
 |-  ( ( x e. S /\ y e. ( ._|_ ` S ) ) -> ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
12 11 adantll
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
13 simplll
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> W e. PreHil )
14 4 sselda
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> y e. V )
15 6 adantr
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> x e. V )
16 8 7 1 9 iporthcom
 |-  ( ( W e. PreHil /\ y e. V /\ x e. V ) -> ( ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) <-> ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
17 13 14 15 16 syl3anc
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> ( ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) <-> ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
18 12 17 mpbid
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
19 18 ralrimiva
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> A. y e. ( ._|_ ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
20 1 7 8 9 2 elocv
 |-  ( x e. ( ._|_ ` ( ._|_ ` S ) ) <-> ( ( ._|_ ` S ) C_ V /\ x e. V /\ A. y e. ( ._|_ ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
21 4 6 19 20 syl3anbrc
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> x e. ( ._|_ ` ( ._|_ ` S ) ) )
22 21 ex
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( x e. S -> x e. ( ._|_ ` ( ._|_ ` S ) ) ) )
23 22 ssrdv
 |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )