Metamath Proof Explorer


Theorem hvsubcl

Description: Closure of vector subtraction. (Contributed by NM, 17-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion hvsubcl ABA-B

Proof

Step Hyp Ref Expression
1 hvsubval ABA-B=A+-1B
2 neg1cn 1
3 hvmulcl 1B-1B
4 2 3 mpan B-1B
5 hvaddcl A-1BA+-1B
6 4 5 sylan2 ABA+-1B
7 1 6 eqeltrd ABA-B