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

Metamath Proof Explorer

Theorem hvpncan3

Description: Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvaddsubass ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ∈ ℋ → A + ℎ B - ℎ A = A + ℎ B - ℎ A
2 1 3anidm13 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ A = A + ℎ B - ℎ A
3 hvpncan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ A = B
4 2 3 eqtr3d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ A = B