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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )

Proof

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