Metamath Proof Explorer

Theorem ocv2ss

Description: Orthocomplements reverse subset inclusion. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypothesis ocv2ss.o 
|- ._|_ = ( ocv ` W )
Assertion ocv2ss 
|- ( T C_ S -> ( ._|_ ` S ) C_ ( ._|_ ` T ) )

Proof

Step Hyp Ref Expression
1 ocv2ss.o 
 |-  ._|_ = ( ocv ` W )
2 sstr2 
 |-  ( T C_ S -> ( S C_ ( Base ` W ) -> T C_ ( Base ` W ) ) )
3 idd 
 |-  ( T C_ S -> ( x e. ( Base ` W ) -> x e. ( Base ` W ) ) )
4 ssralv 
 |-  ( T C_ S -> ( A. y e. S ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) -> A. y e. T ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
5 2 3 4 3anim123d 
 |-  ( T C_ S -> ( ( S C_ ( Base ` W ) /\ x e. ( Base ` W ) /\ A. y e. S ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) -> ( T C_ ( Base ` W ) /\ x e. ( Base ` W ) /\ A. y e. T ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 eqid 
 |-  ( .i ` W ) = ( .i ` W )
8 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
9 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
10 6 7 8 9 1 elocv 
 |-  ( x e. ( ._|_ ` S ) <-> ( S C_ ( Base ` W ) /\ x e. ( Base ` W ) /\ A. y e. S ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
11 6 7 8 9 1 elocv 
 |-  ( x e. ( ._|_ ` T ) <-> ( T C_ ( Base ` W ) /\ x e. ( Base ` W ) /\ A. y e. T ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
12 5 10 11 3imtr4g 
 |-  ( T C_ S -> ( x e. ( ._|_ ` S ) -> x e. ( ._|_ ` T ) ) )
13 12 ssrdv 
 |-  ( T C_ S -> ( ._|_ ` S ) C_ ( ._|_ ` T ) )