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