Theorem hvsubcl

Description: Closure of vector subtraction. (Contributed by NM, 17-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	hvsubcl	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) ∈ ℋ )

Proof

Step	Hyp	Ref	Expression
1		hvsubval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
2		neg1cn	⊢ - 1 ∈ ℂ
3		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ 𝐵 ) ∈ ℋ )
4	2 3	mpan	⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ 𝐵 ) ∈ ℋ )
5		hvaddcl	⊢ ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐵 ) ∈ ℋ ) → ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ ℋ )
6	4 5	sylan2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ ℋ )
7	1 6	eqeltrd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) ∈ ℋ )