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 AB-1AB=AB

Proof

Step Hyp Ref Expression
1 neg1cn 1
2 ax-hvmulass 1AB-1AB=-1AB
3 1 2 mp3an1 AB-1AB=-1AB
4 mulm1 A-1A=A
5 4 adantr AB-1A=A
6 5 oveq1d AB-1AB=AB
7 3 6 eqtr3d AB-1AB=AB