Metamath Proof Explorer

Theorem ellspsn6

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014) (Revised by Mario Carneiro, 8-Jan-2015)

		Ref	Expression
	Hypotheses	ellspsn5b.v	$⊢ V = {Base}_{W}$
		ellspsn5b.s	$⊢ S = LSubSp (W)$
		ellspsn5b.n	$⊢ N = LSpan (W)$
		ellspsn5b.w	$⊢ φ \to W \in LMod$
		ellspsn5b.a	$⊢ φ \to U \in S$
	Assertion	ellspsn6	$⊢ φ \to (X \in U \leftrightarrow (X \in V \land N (\{X\}) \subseteq U))$

Proof

Step	Hyp	Ref	Expression
1		ellspsn5b.v	$⊢ V = {Base}_{W}$
2		ellspsn5b.s	$⊢ S = LSubSp (W)$
3		ellspsn5b.n	$⊢ N = LSpan (W)$
4		ellspsn5b.w	$⊢ φ \to W \in LMod$
5		ellspsn5b.a	$⊢ φ \to U \in S$
6	1 2	lssel	$⊢ (U \in S \land X \in U) \to X \in V$
7	5 6	sylan	$⊢ (φ \land X \in U) \to X \in V$
8	4	adantr	$⊢ (φ \land X \in U) \to W \in LMod$
9	5	adantr	$⊢ (φ \land X \in U) \to U \in S$
10		simpr	$⊢ (φ \land X \in U) \to X \in U$
11	2 3	lspsnss	$⊢ (W \in LMod \land U \in S \land X \in U) \to N (\{X\}) \subseteq U$
12	8 9 10 11	syl3anc	$⊢ (φ \land X \in U) \to N (\{X\}) \subseteq U$
13	7 12	jca	$⊢ (φ \land X \in U) \to (X \in V \land N (\{X\}) \subseteq U)$
14	1 3	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$
15	4 14	sylan	$⊢ (φ \land X \in V) \to X \in N (\{X\})$
16		ssel	$⊢ N (\{X\}) \subseteq U \to (X \in N (\{X\}) \to X \in U)$
17	15 16	syl5com	$⊢ (φ \land X \in V) \to (N (\{X\}) \subseteq U \to X \in U)$
18	17	impr	$⊢ (φ \land (X \in V \land N (\{X\}) \subseteq U)) \to X \in U$
19	13 18	impbida	$⊢ φ \to (X \in U \leftrightarrow (X \in V \land N (\{X\}) \subseteq U))$