Metamath Proof Explorer

Theorem shocorth

Description: Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 shss 
 |-  ( H e. SH -> H C_ ~H )
2 ocorth 
 |-  ( H C_ ~H -> ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( A .ih B ) = 0 ) )
3 1 2 syl 
 |-  ( H e. SH -> ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( A .ih B ) = 0 ) )