lspsn

Description: Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014) (Proof shortened 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	lspsn	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) = \{v \| \exists k \in K v = 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		eqid	$⊢ LSubSp (W) = LSubSp (W)$
7		simpl	$⊢ (W \in LMod \land X \in V) \to W \in LMod$
8	3 1 4 2 6	lss1d	$⊢ (W \in LMod \land X \in V) \to \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \in LSubSp (W)$
9		eqid	$⊢ 1_{F} = 1_{F}$
10	1 2 9	lmod1cl	$⊢ W \in LMod \to 1_{F} \in K$
11	3 1 4 9	lmodvs1	$⊢ (W \in LMod \land X \in V) \to 1_{F} \underset{˙}{\cdot} X = X$
12	11	eqcomd	$⊢ (W \in LMod \land X \in V) \to X = 1_{F} \underset{˙}{\cdot} X$
13		oveq1	$⊢ k = 1_{F} \to k \underset{˙}{\cdot} X = 1_{F} \underset{˙}{\cdot} X$
14	13	rspceeqv	$⊢ (1_{F} \in K \land X = 1_{F} \underset{˙}{\cdot} X) \to \exists k \in K X = k \underset{˙}{\cdot} X$
15	10 12 14	syl2an2r	$⊢ (W \in LMod \land X \in V) \to \exists k \in K X = k \underset{˙}{\cdot} X$
16		eqeq1	$⊢ v = X \to (v = k \underset{˙}{\cdot} X \leftrightarrow X = k \underset{˙}{\cdot} X)$
17	16	rexbidv	$⊢ v = X \to (\exists k \in K v = k \underset{˙}{\cdot} X \leftrightarrow \exists k \in K X = k \underset{˙}{\cdot} X)$
18	17	elabg	$⊢ X \in V \to (X \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \leftrightarrow \exists k \in K X = k \underset{˙}{\cdot} X)$
19	18	adantl	$⊢ (W \in LMod \land X \in V) \to (X \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \leftrightarrow \exists k \in K X = k \underset{˙}{\cdot} X)$
20	15 19	mpbird	$⊢ (W \in LMod \land X \in V) \to X \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}$
21	6 5 7 8 20	ellspsn5	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \subseteq \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}$
22	7	adantr	$⊢ ((W \in LMod \land X \in V) \land k \in K) \to W \in LMod$
23	3 6 5	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
24	23	adantr	$⊢ ((W \in LMod \land X \in V) \land k \in K) \to N (\{X\}) \in LSubSp (W)$
25		simpr	$⊢ ((W \in LMod \land X \in V) \land k \in K) \to k \in K$
26	3 5	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$
27	26	adantr	$⊢ ((W \in LMod \land X \in V) \land k \in K) \to X \in N (\{X\})$
28	1 4 2 6	lssvscl	$⊢ ((W \in LMod \land N (\{X\}) \in LSubSp (W)) \land (k \in K \land X \in N (\{X\}))) \to k \underset{˙}{\cdot} X \in N (\{X\})$
29	22 24 25 27 28	syl22anc	$⊢ ((W \in LMod \land X \in V) \land k \in K) \to k \underset{˙}{\cdot} X \in N (\{X\})$
30		eleq1a	$⊢ k \underset{˙}{\cdot} X \in N (\{X\}) \to (v = k \underset{˙}{\cdot} X \to v \in N (\{X\}))$
31	29 30	syl	$⊢ ((W \in LMod \land X \in V) \land k \in K) \to (v = k \underset{˙}{\cdot} X \to v \in N (\{X\}))$
32	31	rexlimdva	$⊢ (W \in LMod \land X \in V) \to (\exists k \in K v = k \underset{˙}{\cdot} X \to v \in N (\{X\}))$
33	32	abssdv	$⊢ (W \in LMod \land X \in V) \to \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \subseteq N (\{X\})$
34	21 33	eqssd	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) = \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}$

Metamath Proof Explorer

Theorem lspsn

Proof