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