Metamath Proof Explorer


Theorem hvsub32

Description: Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hvsub32 A B C A - B - C = A - C - B

Proof

Step Hyp Ref Expression
1 ax-hvcom B C B + C = C + B
2 1 3adant1 A B C B + C = C + B
3 2 oveq2d A B C A - B + C = A - C + B
4 hvsubass A B C A - B - C = A - B + C
5 hvsubass A C B A - C - B = A - C + B
6 5 3com23 A B C A - C - B = A - C + B
7 3 4 6 3eqtr4d A B C A - B - C = A - C - B