Metamath Proof Explorer

Theorem orthcom

Description: Orthogonality commutes. (Contributed by NM, 10-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion orthcom 
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( ( A .ih B ) = 0 -> ( * ` ( A .ih B ) ) = ( * ` 0 ) )
2 cj0 
 |-  ( * ` 0 ) = 0
3 1 2 eqtrdi 
 |-  ( ( A .ih B ) = 0 -> ( * ` ( A .ih B ) ) = 0 )
4 ax-his1 
 |-  ( ( B e. ~H /\ A e. ~H ) -> ( B .ih A ) = ( * ` ( A .ih B ) ) )
5 4 ancoms 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( B .ih A ) = ( * ` ( A .ih B ) ) )
6 5 eqeq1d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( B .ih A ) = 0 <-> ( * ` ( A .ih B ) ) = 0 ) )
7 3 6 syl5ibr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 -> ( B .ih A ) = 0 ) )
8 fveq2 
 |-  ( ( B .ih A ) = 0 -> ( * ` ( B .ih A ) ) = ( * ` 0 ) )
9 8 2 eqtrdi 
 |-  ( ( B .ih A ) = 0 -> ( * ` ( B .ih A ) ) = 0 )
10 ax-his1 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) )
11 10 eqeq1d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 <-> ( * ` ( B .ih A ) ) = 0 ) )
12 9 11 syl5ibr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( B .ih A ) = 0 -> ( A .ih B ) = 0 ) )
13 7 12 impbid 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 ) )