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