Step |
Hyp |
Ref |
Expression |
1 |
|
neg1cn |
|- -u 1 e. CC |
2 |
|
ax-hvmulass |
|- ( ( -u 1 e. CC /\ A e. CC /\ B e. ~H ) -> ( ( -u 1 x. A ) .h B ) = ( -u 1 .h ( A .h B ) ) ) |
3 |
1 2
|
mp3an1 |
|- ( ( A e. CC /\ B e. ~H ) -> ( ( -u 1 x. A ) .h B ) = ( -u 1 .h ( A .h B ) ) ) |
4 |
|
mulm1 |
|- ( A e. CC -> ( -u 1 x. A ) = -u A ) |
5 |
4
|
adantr |
|- ( ( A e. CC /\ B e. ~H ) -> ( -u 1 x. A ) = -u A ) |
6 |
5
|
oveq1d |
|- ( ( A e. CC /\ B e. ~H ) -> ( ( -u 1 x. A ) .h B ) = ( -u A .h B ) ) |
7 |
3 6
|
eqtr3d |
|- ( ( A e. CC /\ B e. ~H ) -> ( -u 1 .h ( A .h B ) ) = ( -u A .h B ) ) |