Theorem hvsubval

Description: Value of vector subtraction. (Contributed by NM, 5-Sep-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
2		oveq2	⊢ ( 𝑦 = 𝐵 → ( - 1 ·ℎ 𝑦 ) = ( - 1 ·ℎ 𝐵 ) )
3	2	oveq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 +ℎ ( - 1 ·ℎ 𝑦 ) ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
4		df-hvsub	⊢ −ℎ = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
5		ovex	⊢ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ V
6	1 3 4 5	ovmpo	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )