lspsnvsi

Description: Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014) (Proof shortened by Mario Carneiro, 4-Sep-2014)

	Ref	Expression
Hypotheses	lspsn.f	$⊢ F = Scalar (W)$
	lspsn.k	$⊢ K = {Base}_{F}$
	lspsn.v	$⊢ V = {Base}_{W}$
	lspsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lspsn.n	$⊢ N = LSpan (W)$
Assertion	lspsnvsi	$⊢ (W \in LMod \land R \in K \land X \in V) \to N (\{R \underset{˙}{\cdot} X\}) \subseteq N (\{X\})$

Step	Hyp	Ref	Expression
1		lspsn.f	$⊢ F = Scalar (W)$
2		lspsn.k	$⊢ K = {Base}_{F}$
3		lspsn.v	$⊢ V = {Base}_{W}$
4		lspsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		lspsn.n	$⊢ N = LSpan (W)$
6		eqid	$⊢ LSubSp (W) = LSubSp (W)$
7		simp1	$⊢ (W \in LMod \land R \in K \land X \in V) \to W \in LMod$
8		simp3	$⊢ (W \in LMod \land R \in K \land X \in V) \to X \in V$
9	8	snssd	$⊢ (W \in LMod \land R \in K \land X \in V) \to \{X\} \subseteq V$
10	3 6 5	lspcl	$⊢ (W \in LMod \land \{X\} \subseteq V) \to N (\{X\}) \in LSubSp (W)$
11	7 9 10	syl2anc	$⊢ (W \in LMod \land R \in K \land X \in V) \to N (\{X\}) \in LSubSp (W)$
12		simp2	$⊢ (W \in LMod \land R \in K \land X \in V) \to R \in K$
13	3 4 1 2 5 7 12 8	ellspsni	$⊢ (W \in LMod \land R \in K \land X \in V) \to R \underset{˙}{\cdot} X \in N (\{X\})$
14	6 5 7 11 13	ellspsn5	$⊢ (W \in LMod \land R \in K \land X \in V) \to N (\{R \underset{˙}{\cdot} X\}) \subseteq N (\{X\})$

Metamath Proof Explorer