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