Metamath Proof Explorer


Theorem hvsubass

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

Ref Expression
Assertion hvsubass A B C A - B - C = A - B + C

Proof

Step Hyp Ref Expression
1 neg1cn 1
2 hvmulcl 1 B -1 B
3 1 2 mpan B -1 B
4 hvaddsubass A -1 B C A + -1 B - C = A + -1 B - C
5 3 4 syl3an2 A B C A + -1 B - C = A + -1 B - C
6 hvsubval A B A - B = A + -1 B
7 6 3adant3 A B C A - B = A + -1 B
8 7 oveq1d A B C A - B - C = A + -1 B - C
9 simp1 A B C A
10 hvaddcl B C B + C
11 10 3adant1 A B C B + C
12 hvsubval A B + C A - B + C = A + -1 B + C
13 9 11 12 syl2anc A B C A - B + C = A + -1 B + C
14 hvsubval -1 B C -1 B - C = -1 B + -1 C
15 3 14 sylan B C -1 B - C = -1 B + -1 C
16 15 3adant1 A B C -1 B - C = -1 B + -1 C
17 ax-hvdistr1 1 B C -1 B + C = -1 B + -1 C
18 1 17 mp3an1 B C -1 B + C = -1 B + -1 C
19 18 3adant1 A B C -1 B + C = -1 B + -1 C
20 16 19 eqtr4d A B C -1 B - C = -1 B + C
21 20 oveq2d A B C A + -1 B - C = A + -1 B + C
22 13 21 eqtr4d A B C A - B + C = A + -1 B - C
23 5 8 22 3eqtr4d A B C A - B - C = A - B + C