ellspsni

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

Step	Hyp	Ref	Expression
1		lspsnvsel.v	$⊢ V = {Base}_{W}$
2		lspsnvsel.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		lspsnvsel.f	$⊢ F = Scalar (W)$
4		lspsnvsel.k	$⊢ K = {Base}_{F}$
5		lspsnvsel.n	$⊢ N = LSpan (W)$
6		lspsnvsel.w	$⊢ φ \to W \in LMod$
7		lspsnvsel.a	$⊢ φ \to A \in K$
8		lspsnvsel.x	$⊢ φ \to X \in V$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10	1 9 5	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
11	6 8 10	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (W)$
12	1 5	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$
13	6 8 12	syl2anc	$⊢ φ \to X \in N (\{X\})$
14	3 2 4 9	lssvscl	$⊢ ((W \in LMod \land N (\{X\}) \in LSubSp (W)) \land (A \in K \land X \in N (\{X\}))) \to A \underset{˙}{\cdot} X \in N (\{X\})$
15	6 11 7 13 14	syl22anc	$⊢ φ \to A \underset{˙}{\cdot} X \in N (\{X\})$

Metamath Proof Explorer