lspprat

Description: A proper subspace of the span of a pair of vectors is the span of a singleton (an atom) or the zero subspace (if z is zero). Proof suggested by Mario Carneiro, 28-Aug-2014. (Contributed by NM, 29-Aug-2014)

	Ref	Expression
Hypotheses	lspprat.v	$⊢ V = {Base}_{W}$
	lspprat.s	$⊢ S = LSubSp (W)$
	lspprat.n	$⊢ N = LSpan (W)$
	lspprat.w	$⊢ φ \to W \in LVec$
	lspprat.u	$⊢ φ \to U \in S$
	lspprat.x	$⊢ φ \to X \in V$
	lspprat.y	$⊢ φ \to Y \in V$
	lspprat.p	$⊢ φ \to U \subset N (\{X, Y\})$
Assertion	lspprat	$⊢ φ \to \exists z \in V U = N (\{z\})$

Proof

Step	Hyp	Ref	Expression
1		lspprat.v	$⊢ V = {Base}_{W}$
2		lspprat.s	$⊢ S = LSubSp (W)$
3		lspprat.n	$⊢ N = LSpan (W)$
4		lspprat.w	$⊢ φ \to W \in LVec$
5		lspprat.u	$⊢ φ \to U \in S$
6		lspprat.x	$⊢ φ \to X \in V$
7		lspprat.y	$⊢ φ \to Y \in V$
8		lspprat.p	$⊢ φ \to U \subset N (\{X, Y\})$
9		ssdif0	$⊢ U \subseteq \{0_{W}\} \leftrightarrow U ∖ \{0_{W}\} = \emptyset$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	4 10	syl	$⊢ φ \to W \in LMod$
12		eqid	$⊢ 0_{W} = 0_{W}$
13	1 12	lmod0vcl	$⊢ W \in LMod \to 0_{W} \in V$
14	11 13	syl	$⊢ φ \to 0_{W} \in V$
15	14	adantr	$⊢ (φ \land U \subseteq \{0_{W}\}) \to 0_{W} \in V$
16		simpr	$⊢ (φ \land U \subseteq \{0_{W}\}) \to U \subseteq \{0_{W}\}$
17	12 2	lss0ss	$⊢ (W \in LMod \land U \in S) \to \{0_{W}\} \subseteq U$
18	11 5 17	syl2anc	$⊢ φ \to \{0_{W}\} \subseteq U$
19	18	adantr	$⊢ (φ \land U \subseteq \{0_{W}\}) \to \{0_{W}\} \subseteq U$
20	16 19	eqssd	$⊢ (φ \land U \subseteq \{0_{W}\}) \to U = \{0_{W}\}$
21	12 3	lspsn0	$⊢ W \in LMod \to N (\{0_{W}\}) = \{0_{W}\}$
22	11 21	syl	$⊢ φ \to N (\{0_{W}\}) = \{0_{W}\}$
23	22	adantr	$⊢ (φ \land U \subseteq \{0_{W}\}) \to N (\{0_{W}\}) = \{0_{W}\}$
24	20 23	eqtr4d	$⊢ (φ \land U \subseteq \{0_{W}\}) \to U = N (\{0_{W}\})$
25		sneq	$⊢ z = 0_{W} \to \{z\} = \{0_{W}\}$
26	25	fveq2d	$⊢ z = 0_{W} \to N (\{z\}) = N (\{0_{W}\})$
27	26	rspceeqv	$⊢ (0_{W} \in V \land U = N (\{0_{W}\})) \to \exists z \in V U = N (\{z\})$
28	15 24 27	syl2anc	$⊢ (φ \land U \subseteq \{0_{W}\}) \to \exists z \in V U = N (\{z\})$
29	28	ex	$⊢ φ \to (U \subseteq \{0_{W}\} \to \exists z \in V U = N (\{z\}))$
30	9 29	biimtrrid	$⊢ φ \to (U ∖ \{0_{W}\} = \emptyset \to \exists z \in V U = N (\{z\}))$
31	1 2	lssss	$⊢ U \in S \to U \subseteq V$
32	5 31	syl	$⊢ φ \to U \subseteq V$
33	32	ssdifssd	$⊢ φ \to U ∖ \{0_{W}\} \subseteq V$
34	33	sseld	$⊢ φ \to (z \in (U ∖ \{0_{W}\}) \to z \in V)$
35	1 2 3 4 5 6 7 8 12	lsppratlem6	$⊢ φ \to (z \in (U ∖ \{0_{W}\}) \to U = N (\{z\}))$
36	34 35	jcad	$⊢ φ \to (z \in (U ∖ \{0_{W}\}) \to (z \in V \land U = N (\{z\})))$
37	36	eximdv	$⊢ φ \to (\exists z z \in (U ∖ \{0_{W}\}) \to \exists z (z \in V \land U = N (\{z\})))$
38		n0	$⊢ U ∖ \{0_{W}\} \neq \emptyset \leftrightarrow \exists z z \in (U ∖ \{0_{W}\})$
39		df-rex	$⊢ \exists z \in V U = N (\{z\}) \leftrightarrow \exists z (z \in V \land U = N (\{z\}))$
40	37 38 39	3imtr4g	$⊢ φ \to (U ∖ \{0_{W}\} \neq \emptyset \to \exists z \in V U = N (\{z\}))$
41	30 40	pm2.61dne	$⊢ φ \to \exists z \in V U = N (\{z\})$

Metamath Proof Explorer

Theorem lspprat

Proof