Metamath Proof Explorer

Theorem abshicom

Description: Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion abshicom 
|- ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( A .ih B ) ) = ( abs ` ( B .ih A ) ) )

Proof

Step Hyp Ref Expression
1 ax-his1 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) )
2 1 fveq2d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( A .ih B ) ) = ( abs ` ( * ` ( B .ih A ) ) ) )
3 hicl 
 |-  ( ( B e. ~H /\ A e. ~H ) -> ( B .ih A ) e. CC )
4 3 ancoms 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( B .ih A ) e. CC )
5 4 abscjd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( * ` ( B .ih A ) ) ) = ( abs ` ( B .ih A ) ) )
6 2 5 eqtrd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( A .ih B ) ) = ( abs ` ( B .ih A ) ) )