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

Metamath Proof Explorer

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