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	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ·ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		spansnsh	⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ Sℋ )
2		spansnid	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) )
3	1 2	jca	⊢ ( 𝐴 ∈ ℋ → ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ 𝐴 ∈ ( span ‘ { 𝐴 } ) ) )
4		shmulcl	⊢ ( ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ( span ‘ { 𝐴 } ) ) → ( 𝐵 ·ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) )
5	4	3com12	⊢ ( ( 𝐵 ∈ ℂ ∧ ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ 𝐴 ∈ ( span ‘ { 𝐴 } ) ) → ( 𝐵 ·ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) )
6	5	3expb	⊢ ( ( 𝐵 ∈ ℂ ∧ ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ 𝐴 ∈ ( span ‘ { 𝐴 } ) ) ) → ( 𝐵 ·ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) )
7	3 6	sylan2	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) )
8	7	ancoms	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ·ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) )