lspsnat

Description: There is no subspace strictly between the zero subspace and the span of a vector (i.e. a 1-dimensional subspace is an atom). ( h1datomi analog.) (Contributed by NM, 20-Apr-2014) (Proof shortened by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	lspsnat.v	$⊢ V = {Base}_{W}$
	lspsnat.z	$⊢ \underset{˙}{0} = 0_{W}$
	lspsnat.s	$⊢ S = LSubSp (W)$
	lspsnat.n	$⊢ N = LSpan (W)$
Assertion	lspsnat	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (U = N (\{X\}) \lor U = \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		lspsnat.v	$⊢ V = {Base}_{W}$
2		lspsnat.z	$⊢ \underset{˙}{0} = 0_{W}$
3		lspsnat.s	$⊢ S = LSubSp (W)$
4		lspsnat.n	$⊢ N = LSpan (W)$
5		n0	$⊢ U ∖ \{\underset{˙}{0}\} \neq \emptyset \leftrightarrow \exists x x \in (U ∖ \{\underset{˙}{0}\})$
6		simprl	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to U \subseteq N (\{X\})$
7		simpl1	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to W \in LVec$
8		lveclmod	$⊢ W \in LVec \to W \in LMod$
9	7 8	syl	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to W \in LMod$
10		simpl2	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to U \in S$
11		simprr	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to x \in (U ∖ \{\underset{˙}{0}\})$
12	11	eldifad	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to x \in U$
13	3 4 9 10 12	lspsnel5a	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to N (\{x\}) \subseteq U$
14		0ss	$⊢ \emptyset \subseteq V$
15	14	a1i	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to \emptyset \subseteq V$
16		simpl3	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to X \in V$
17		ssdif	$⊢ U \subseteq N (\{X\}) \to U ∖ \{\underset{˙}{0}\} \subseteq N (\{X\}) ∖ \{\underset{˙}{0}\}$
18	17	ad2antrl	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to U ∖ \{\underset{˙}{0}\} \subseteq N (\{X\}) ∖ \{\underset{˙}{0}\}$
19	18 11	sseldd	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to x \in (N (\{X\}) ∖ \{\underset{˙}{0}\})$
20		uncom	$⊢ \emptyset \cup \{X\} = \{X\} \cup \emptyset$
21		un0	$⊢ \{X\} \cup \emptyset = \{X\}$
22	20 21	eqtri	$⊢ \emptyset \cup \{X\} = \{X\}$
23	22	fveq2i	$⊢ N (\emptyset \cup \{X\}) = N (\{X\})$
24	23	a1i	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to N (\emptyset \cup \{X\}) = N (\{X\})$
25	2 4	lsp0	$⊢ W \in LMod \to N (\emptyset) = \{\underset{˙}{0}\}$
26	9 25	syl	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to N (\emptyset) = \{\underset{˙}{0}\}$
27	24 26	difeq12d	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to N (\emptyset \cup \{X\}) ∖ N (\emptyset) = N (\{X\}) ∖ \{\underset{˙}{0}\}$
28	19 27	eleqtrrd	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to x \in (N (\emptyset \cup \{X\}) ∖ N (\emptyset))$
29	1 3 4	lspsolv	$⊢ (W \in LVec \land (\emptyset \subseteq V \land X \in V \land x \in (N (\emptyset \cup \{X\}) ∖ N (\emptyset)))) \to X \in N (\emptyset \cup \{x\})$
30	7 15 16 28 29	syl13anc	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to X \in N (\emptyset \cup \{x\})$
31		uncom	$⊢ \emptyset \cup \{x\} = \{x\} \cup \emptyset$
32		un0	$⊢ \{x\} \cup \emptyset = \{x\}$
33	31 32	eqtri	$⊢ \emptyset \cup \{x\} = \{x\}$
34	33	fveq2i	$⊢ N (\emptyset \cup \{x\}) = N (\{x\})$
35	30 34	eleqtrdi	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to X \in N (\{x\})$
36	13 35	sseldd	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to X \in U$
37	3 4 9 10 36	lspsnel5a	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to N (\{X\}) \subseteq U$
38	6 37	eqssd	$⊢ ((W \in LVec \land U \in S \land X \in V) \land (U \subseteq N (\{X\}) \land x \in (U ∖ \{\underset{˙}{0}\}))) \to U = N (\{X\})$
39	38	expr	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (x \in (U ∖ \{\underset{˙}{0}\}) \to U = N (\{X\}))$
40	39	exlimdv	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (\exists x x \in (U ∖ \{\underset{˙}{0}\}) \to U = N (\{X\}))$
41	5 40	syl5bi	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (U ∖ \{\underset{˙}{0}\} \neq \emptyset \to U = N (\{X\}))$
42	41	necon1bd	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (\neg U = N (\{X\}) \to U ∖ \{\underset{˙}{0}\} = \emptyset)$
43		ssdif0	$⊢ U \subseteq \{\underset{˙}{0}\} \leftrightarrow U ∖ \{\underset{˙}{0}\} = \emptyset$
44	42 43	syl6ibr	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (\neg U = N (\{X\}) \to U \subseteq \{\underset{˙}{0}\})$
45		simpl1	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to W \in LVec$
46	45 8	syl	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to W \in LMod$
47		simpl2	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to U \in S$
48	2 3	lssle0	$⊢ (W \in LMod \land U \in S) \to (U \subseteq \{\underset{˙}{0}\} \leftrightarrow U = \{\underset{˙}{0}\})$
49	46 47 48	syl2anc	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (U \subseteq \{\underset{˙}{0}\} \leftrightarrow U = \{\underset{˙}{0}\})$
50	44 49	sylibd	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (\neg U = N (\{X\}) \to U = \{\underset{˙}{0}\})$
51	50	orrd	$⊢ ((W \in LVec \land U \in S \land X \in V) \land U \subseteq N (\{X\})) \to (U = N (\{X\}) \lor U = \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem lspsnat

Proof