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