Metamath Proof Explorer

Theorem lspsnel

Description: Member of span of the singleton of a vector. ( elspansn analog.) (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Jun-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	lspsnel	$⊢ (W \in LMod \land X \in V) \to (U \in N (\{X\}) \leftrightarrow \exists k \in K U = k \underset{˙}{\cdot} X)$

Proof

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	1 2 3 4 5	lspsn	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) = \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}$
7	6	eleq2d	$⊢ (W \in LMod \land X \in V) \to (U \in N (\{X\}) \leftrightarrow U \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\})$
8		id	$⊢ U = k \underset{˙}{\cdot} X \to U = k \underset{˙}{\cdot} X$
9		ovex	$⊢ k \underset{˙}{\cdot} X \in V$
10	8 9	eqeltrdi	$⊢ U = k \underset{˙}{\cdot} X \to U \in V$
11	10	rexlimivw	$⊢ \exists k \in K U = k \underset{˙}{\cdot} X \to U \in V$
12		eqeq1	$⊢ v = U \to (v = k \underset{˙}{\cdot} X \leftrightarrow U = k \underset{˙}{\cdot} X)$
13	12	rexbidv	$⊢ v = U \to (\exists k \in K v = k \underset{˙}{\cdot} X \leftrightarrow \exists k \in K U = k \underset{˙}{\cdot} X)$
14	11 13	elab3	$⊢ U \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \leftrightarrow \exists k \in K U = k \underset{˙}{\cdot} X$
15	7 14	bitrdi	$⊢ (W \in LMod \land X \in V) \to (U \in N (\{X\}) \leftrightarrow \exists k \in K U = k \underset{˙}{\cdot} X)$