Metamath Proof Explorer

Theorem hvm1neg

Description: Convert minus one times a scalar product to the negative of the scalar. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion hvm1neg 
|- ( ( A e. CC /\ B e. ~H ) -> ( -u 1 .h ( A .h B ) ) = ( -u A .h B ) )

Proof

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