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

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