This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid 
 |-  ( 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 imbitrrdi 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A C_ ( _|_ ` B ) -> ( A i^i B ) = 0H ) )