Metamath Proof Explorer

Theorem ocvsscon

Description: Two ways to say that S and T are orthogonal subspaces. (Contributed by Mario Carneiro, 23-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 ocvlsp.v 
 |-  V = ( Base ` W )
2 ocvlsp.o 
 |-  ._|_ = ( ocv ` W )
3 1 2 ocvocv 
 |-  ( ( W e. PreHil /\ T C_ V ) -> T C_ ( ._|_ ` ( ._|_ ` T ) ) )
4 3 3adant2 
 |-  ( ( W e. PreHil /\ S C_ V /\ T C_ V ) -> T C_ ( ._|_ ` ( ._|_ ` T ) ) )
5 2 ocv2ss 
 |-  ( S C_ ( ._|_ ` T ) -> ( ._|_ ` ( ._|_ ` T ) ) C_ ( ._|_ ` S ) )
6 sstr2 
 |-  ( T C_ ( ._|_ ` ( ._|_ ` T ) ) -> ( ( ._|_ ` ( ._|_ ` T ) ) C_ ( ._|_ ` S ) -> T C_ ( ._|_ ` S ) ) )
7 4 5 6 syl2im 
 |-  ( ( W e. PreHil /\ S C_ V /\ T C_ V ) -> ( S C_ ( ._|_ ` T ) -> T C_ ( ._|_ ` S ) ) )
8 1 2 ocvocv 
 |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )
9 8 3adant3 
 |-  ( ( W e. PreHil /\ S C_ V /\ T C_ V ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )
10 2 ocv2ss 
 |-  ( T C_ ( ._|_ ` S ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ ( ._|_ ` T ) )
11 sstr2 
 |-  ( S C_ ( ._|_ ` ( ._|_ ` S ) ) -> ( ( ._|_ ` ( ._|_ ` S ) ) C_ ( ._|_ ` T ) -> S C_ ( ._|_ ` T ) ) )
12 9 10 11 syl2im 
 |-  ( ( W e. PreHil /\ S C_ V /\ T C_ V ) -> ( T C_ ( ._|_ ` S ) -> S C_ ( ._|_ ` T ) ) )
13 7 12 impbid 
 |-  ( ( W e. PreHil /\ S C_ V /\ T C_ V ) -> ( S C_ ( ._|_ ` T ) <-> T C_ ( ._|_ ` S ) ) )