Metamath Proof Explorer

Theorem spansnmul

Description: A scalar product with a vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnmul ⊢ A ∈ ℋ ∧ B ∈ ℂ → B ⋅ ℎ A ∈ span ⁡ A

Proof

Step Hyp Ref Expression
1 spansnsh ⊢ A ∈ ℋ → span ⁡ A ∈ S ℋ
2 spansnid ⊢ A ∈ ℋ → A ∈ span ⁡ A
3 1 2 jca ⊢ A ∈ ℋ → span ⁡ A ∈ S ℋ ∧ A ∈ span ⁡ A
4 shmulcl ⊢ span ⁡ A ∈ S ℋ ∧ B ∈ ℂ ∧ A ∈ span ⁡ A → B ⋅ ℎ A ∈ span ⁡ A
5 4 3com12 ⊢ B ∈ ℂ ∧ span ⁡ A ∈ S ℋ ∧ A ∈ span ⁡ A → B ⋅ ℎ A ∈ span ⁡ A
6 5 3expb ⊢ B ∈ ℂ ∧ span ⁡ A ∈ S ℋ ∧ A ∈ span ⁡ A → B ⋅ ℎ A ∈ span ⁡ A
7 3 6 sylan2 ⊢ B ∈ ℂ ∧ A ∈ ℋ → B ⋅ ℎ A ∈ span ⁡ A
8 7 ancoms ⊢ A ∈ ℋ ∧ B ∈ ℂ → B ⋅ ℎ A ∈ span ⁡ A