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

Metamath Proof Explorer

Theorem hvpncan2

Description: Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax-hvcom ⊢ B ∈ ℋ ∧ A ∈ ℋ → B + ℎ A = A + ℎ B
2 1 oveq1d ⊢ B ∈ ℋ ∧ A ∈ ℋ → B + ℎ A - ℎ A = A + ℎ B - ℎ A
3 hvpncan ⊢ B ∈ ℋ ∧ A ∈ ℋ → B + ℎ A - ℎ A = B
4 2 3 eqtr3d ⊢ B ∈ ℋ ∧ A ∈ ℋ → A + ℎ B - ℎ A = B
5 4 ancoms ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ A = B