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