Theorem ellspsni

Description: A scalar product with a vector belongs to the span of its singleton. ( spansnmul analog.) (Contributed by NM, 2-Jul-2014)

	Ref	Expression
Hypotheses	lspsnvsel.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspsnvsel.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lspsnvsel.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lspsnvsel.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lspsnvsel.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspsnvsel.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lspsnvsel.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	lspsnvsel.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	ellspsni	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		lspsnvsel.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsnvsel.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		lspsnvsel.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		lspsnvsel.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lspsnvsel.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
6		lspsnvsel.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7		lspsnvsel.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
8		lspsnvsel.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10	1 9 5	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
11	6 8 10	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
12	1 5	lspsnid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
13	6 8 12	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
14	3 2 4 9	lssvscl	⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )
15	6 11 7 13 14	syl22anc	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )