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 ) ) )