Metamath Proof Explorer


Theorem orthin

Description: The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion orthin
|- ( ( A e. SH /\ B e. SH ) -> ( A C_ ( _|_ ` B ) -> ( A i^i B ) = 0H ) )

Proof

Step Hyp Ref Expression
1 ssrin
 |-  ( A C_ ( _|_ ` B ) -> ( A i^i B ) C_ ( ( _|_ ` B ) i^i B ) )
2 incom
 |-  ( ( _|_ ` B ) i^i B ) = ( B i^i ( _|_ ` B ) )
3 1 2 sseqtrdi
 |-  ( A C_ ( _|_ ` B ) -> ( A i^i B ) C_ ( B i^i ( _|_ ` B ) ) )
4 ocin
 |-  ( B e. SH -> ( B i^i ( _|_ ` B ) ) = 0H )
5 4 sseq2d
 |-  ( B e. SH -> ( ( A i^i B ) C_ ( B i^i ( _|_ ` B ) ) <-> ( A i^i B ) C_ 0H ) )
6 3 5 syl5ib
 |-  ( B e. SH -> ( A C_ ( _|_ ` B ) -> ( A i^i B ) C_ 0H ) )
7 6 adantl
 |-  ( ( A e. SH /\ B e. SH ) -> ( A C_ ( _|_ ` B ) -> ( A i^i B ) C_ 0H ) )
8 shincl
 |-  ( ( A e. SH /\ B e. SH ) -> ( A i^i B ) e. SH )
9 sh0le
 |-  ( ( A i^i B ) e. SH -> 0H C_ ( A i^i B ) )
10 8 9 syl
 |-  ( ( A e. SH /\ B e. SH ) -> 0H C_ ( A i^i B ) )
11 7 10 jctird
 |-  ( ( A e. SH /\ B e. SH ) -> ( A C_ ( _|_ ` B ) -> ( ( A i^i B ) C_ 0H /\ 0H C_ ( A i^i B ) ) ) )
12 eqss
 |-  ( ( A i^i B ) = 0H <-> ( ( A i^i B ) C_ 0H /\ 0H C_ ( A i^i B ) ) )
13 11 12 syl6ibr
 |-  ( ( A e. SH /\ B e. SH ) -> ( A C_ ( _|_ ` B ) -> ( A i^i B ) = 0H ) )