Theorem shorth

Description: Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	shorth	|- ( H e. SH -> ( G C_ ( _|_ ` H ) -> ( ( A e. G /\ B e. H ) -> ( A .ih B ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( G C_ ( _|_ ` H ) -> ( A e. G -> A e. ( _|_ ` H ) ) )
2	1	anim1d	|- ( G C_ ( _|_ ` H ) -> ( ( A e. G /\ B e. H ) -> ( A e. ( _|_ ` H ) /\ B e. H ) ) )
3	2	imp	|- ( ( G C_ ( _|_ ` H ) /\ ( A e. G /\ B e. H ) ) -> ( A e. ( _|_ ` H ) /\ B e. H ) )
4	3	ancomd	|- ( ( G C_ ( _|_ ` H ) /\ ( A e. G /\ B e. H ) ) -> ( B e. H /\ A e. ( _|_ ` H ) ) )
5		shocorth	|- ( H e. SH -> ( ( B e. H /\ A e. ( _|_ ` H ) ) -> ( B .ih A ) = 0 ) )
6	5	imp	|- ( ( H e. SH /\ ( B e. H /\ A e. ( _|_ ` H ) ) ) -> ( B .ih A ) = 0 )
7		shss	|- ( H e. SH -> H C_ ~H )
8	7	sseld	|- ( H e. SH -> ( B e. H -> B e. ~H ) )
9		shocss	|- ( H e. SH -> ( _|_ ` H ) C_ ~H )
10	9	sseld	|- ( H e. SH -> ( A e. ( _|_ ` H ) -> A e. ~H ) )
11	8 10	anim12d	|- ( H e. SH -> ( ( B e. H /\ A e. ( _|_ ` H ) ) -> ( B e. ~H /\ A e. ~H ) ) )
12	11	imp	|- ( ( H e. SH /\ ( B e. H /\ A e. ( _|_ ` H ) ) ) -> ( B e. ~H /\ A e. ~H ) )
13		orthcom	|- ( ( B e. ~H /\ A e. ~H ) -> ( ( B .ih A ) = 0 <-> ( A .ih B ) = 0 ) )
14	12 13	syl	|- ( ( H e. SH /\ ( B e. H /\ A e. ( _|_ ` H ) ) ) -> ( ( B .ih A ) = 0 <-> ( A .ih B ) = 0 ) )
15	6 14	mpbid	|- ( ( H e. SH /\ ( B e. H /\ A e. ( _|_ ` H ) ) ) -> ( A .ih B ) = 0 )
16	4 15	sylan2	|- ( ( H e. SH /\ ( G C_ ( _|_ ` H ) /\ ( A e. G /\ B e. H ) ) ) -> ( A .ih B ) = 0 )
17	16	exp32	|- ( H e. SH -> ( G C_ ( _|_ ` H ) -> ( ( A e. G /\ B e. H ) -> ( A .ih B ) = 0 ) ) )