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