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