Metamath Proof Explorer

Theorem hvsubcl

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

Ref Expression
Assertion hvsubcl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ∈ ℋ

Proof

Step Hyp Ref Expression
1 hvsubval ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B = A + ℎ -1 ⋅ ℎ B
2 neg1cn ⊢ − 1 ∈ ℂ
3 hvmulcl ⊢ − 1 ∈ ℂ ∧ B ∈ ℋ → -1 ⋅ ℎ B ∈ ℋ
4 2 3 mpan ⊢ B ∈ ℋ → -1 ⋅ ℎ B ∈ ℋ
5 hvaddcl ⊢ A ∈ ℋ ∧ -1 ⋅ ℎ B ∈ ℋ → A + ℎ -1 ⋅ ℎ B ∈ ℋ
6 4 5 sylan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ -1 ⋅ ℎ B ∈ ℋ
7 1 6 eqeltrd ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ∈ ℋ