Metamath Proof Explorer

Theorem hvpncan

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

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

Proof

Step Hyp Ref Expression
1 hvaddcl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B ∈ ℋ
2 hvsubval ⊢ A + ℎ B ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ B = A + ℎ B + ℎ -1 ⋅ ℎ B
3 1 2 sylancom ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ B = A + ℎ B + ℎ -1 ⋅ ℎ B
4 neg1cn ⊢ − 1 ∈ ℂ
5 hvmulcl ⊢ − 1 ∈ ℂ ∧ B ∈ ℋ → -1 ⋅ ℎ B ∈ ℋ
6 4 5 mpan ⊢ B ∈ ℋ → -1 ⋅ ℎ B ∈ ℋ
7 6 ancli ⊢ B ∈ ℋ → B ∈ ℋ ∧ -1 ⋅ ℎ B ∈ ℋ
8 ax-hvass ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ B ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ B = A + ℎ B + ℎ -1 ⋅ ℎ B
9 8 3expb ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ B ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ B = A + ℎ B + ℎ -1 ⋅ ℎ B
10 7 9 sylan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ B = A + ℎ B + ℎ -1 ⋅ ℎ B
11 hvnegid ⊢ B ∈ ℋ → B + ℎ -1 ⋅ ℎ B = 0 ℎ
12 11 oveq2d ⊢ B ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ B = A + ℎ 0 ℎ
13 ax-hvaddid ⊢ A ∈ ℋ → A + ℎ 0 ℎ = A
14 12 13 sylan9eqr ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ B = A
15 3 10 14 3eqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ B = A