This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hvaddsubass

Description: Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

Ref Expression
Assertion hvaddsubass ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = A + ℎ B - ℎ C

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ − 1 ∈ ℂ
2 hvmulcl ⊢ − 1 ∈ ℂ ∧ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
3 1 2 mpan ⊢ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
4 ax-hvass ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ C ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ C = A + ℎ B + ℎ -1 ⋅ ℎ C
5 3 4 syl3an3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ C = A + ℎ B + ℎ -1 ⋅ ℎ C
6 hvaddcl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B ∈ ℋ
7 hvsubval ⊢ A + ℎ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = A + ℎ B + ℎ -1 ⋅ ℎ C
8 6 7 stoic3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = A + ℎ B + ℎ -1 ⋅ ℎ C
9 hvsubval ⊢ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C = B + ℎ -1 ⋅ ℎ C
10 9 3adant1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C = B + ℎ -1 ⋅ ℎ C
11 10 oveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = A + ℎ B + ℎ -1 ⋅ ℎ C
12 5 8 11 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = A + ℎ B - ℎ C