Theorem hvaddsubval

Description: Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hvaddsubval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 −ℎ ( - 1 ·ℎ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		neg1cn	⊢ - 1 ∈ ℂ
2		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ 𝐵 ) ∈ ℋ )
3	1 2	mpan	⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ 𝐵 ) ∈ ℋ )
4		hvsubval	⊢ ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) → ( 𝐴 −ℎ ( - 1 ·ℎ 𝐵 ) ) = ( 𝐴 +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ) )
5	3 4	sylan2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ ( - 1 ·ℎ 𝐵 ) ) = ( 𝐴 +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ) )
6		hvm1neg	⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) = ( - - 1 ·ℎ 𝐵 ) )
7	1 6	mpan	⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) = ( - - 1 ·ℎ 𝐵 ) )
8		negneg1e1	⊢ - - 1 = 1
9	8	oveq1i	⊢ ( - - 1 ·ℎ 𝐵 ) = ( 1 ·ℎ 𝐵 )
10	7 9	eqtrdi	⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) = ( 1 ·ℎ 𝐵 ) )
11		ax-hvmulid	⊢ ( 𝐵 ∈ ℋ → ( 1 ·ℎ 𝐵 ) = 𝐵 )
12	10 11	eqtrd	⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐵 )
13	12	adantl	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐵 )
14	13	oveq2d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐴 +ℎ 𝐵 ) )
15	5 14	eqtr2d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 −ℎ ( - 1 ·ℎ 𝐵 ) ) )