ellspsn4

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. ( elspansn4 analog.) (Contributed by NM, 4-Jul-2014)

	Ref	Expression
Hypotheses	ellspsn4.v	$⊢ V = {Base}_{W}$
	ellspsn4.o	$⊢ \underset{˙}{0} = 0_{W}$
	ellspsn4.s	$⊢ S = LSubSp (W)$
	ellspsn4.n	$⊢ N = LSpan (W)$
	ellspsn4.w	$⊢ φ \to W \in LVec$
	ellspsn4.u	$⊢ φ \to U \in S$
	ellspsn4.x	$⊢ φ \to X \in V$
	ellspsn4.y	$⊢ φ \to Y \in N (\{X\})$
	ellspsn4.z	$⊢ φ \to Y \neq \underset{˙}{0}$
Assertion	ellspsn4	$⊢ φ \to (X \in U \leftrightarrow Y \in U)$

Proof

Step	Hyp	Ref	Expression
1		ellspsn4.v	$⊢ V = {Base}_{W}$
2		ellspsn4.o	$⊢ \underset{˙}{0} = 0_{W}$
3		ellspsn4.s	$⊢ S = LSubSp (W)$
4		ellspsn4.n	$⊢ N = LSpan (W)$
5		ellspsn4.w	$⊢ φ \to W \in LVec$
6		ellspsn4.u	$⊢ φ \to U \in S$
7		ellspsn4.x	$⊢ φ \to X \in V$
8		ellspsn4.y	$⊢ φ \to Y \in N (\{X\})$
9		ellspsn4.z	$⊢ φ \to Y \neq \underset{˙}{0}$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	5 10	syl	$⊢ φ \to W \in LMod$
12	11	adantr	$⊢ (φ \land X \in U) \to W \in LMod$
13	6	adantr	$⊢ (φ \land X \in U) \to U \in S$
14		simpr	$⊢ (φ \land X \in U) \to X \in U$
15	8	adantr	$⊢ (φ \land X \in U) \to Y \in N (\{X\})$
16	3 4 12 13 14 15	ellspsn3	$⊢ (φ \land X \in U) \to Y \in U$
17	11	adantr	$⊢ (φ \land Y \in U) \to W \in LMod$
18	6	adantr	$⊢ (φ \land Y \in U) \to U \in S$
19		simpr	$⊢ (φ \land Y \in U) \to Y \in U$
20	1 4	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$
21	11 7 20	syl2anc	$⊢ φ \to X \in N (\{X\})$
22	1 2 4 5 7 8 9	lspsneleq	$⊢ φ \to N (\{Y\}) = N (\{X\})$
23	21 22	eleqtrrd	$⊢ φ \to X \in N (\{Y\})$
24	23	adantr	$⊢ (φ \land Y \in U) \to X \in N (\{Y\})$
25	3 4 17 18 19 24	ellspsn3	$⊢ (φ \land Y \in U) \to X \in U$
26	16 25	impbida	$⊢ φ \to (X \in U \leftrightarrow Y \in U)$

Metamath Proof Explorer

Theorem ellspsn4

Proof