lsatelbN

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		lsatelb.v	$⊢ V = {Base}_{W}$
2		lsatelb.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lsatelb.n	$⊢ N = LSpan (W)$
4		lsatelb.a	$⊢ A = LSAtoms (W)$
5		lsatelb.w	$⊢ φ \to W \in LVec$
6		lsatelb.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
7		lsatelb.u	$⊢ φ \to U \in A$
8	5	adantr	$⊢ (φ \land X \in U) \to W \in LVec$
9	7	adantr	$⊢ (φ \land X \in U) \to U \in A$
10		simpr	$⊢ (φ \land X \in U) \to X \in U$
11		eldifsn	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in V \land X \neq \underset{˙}{0})$
12	6 11	sylib	$⊢ φ \to (X \in V \land X \neq \underset{˙}{0})$
13	12	simprd	$⊢ φ \to X \neq \underset{˙}{0}$
14	13	adantr	$⊢ (φ \land X \in U) \to X \neq \underset{˙}{0}$
15	2 3 4 8 9 10 14	lsatel	$⊢ (φ \land X \in U) \to U = N (\{X\})$
16		eqimss2	$⊢ U = N (\{X\}) \to N (\{X\}) \subseteq U$
17	16	adantl	$⊢ (φ \land U = N (\{X\})) \to N (\{X\}) \subseteq U$
18		eqid	$⊢ LSubSp (W) = LSubSp (W)$
19		lveclmod	$⊢ W \in LVec \to W \in LMod$
20	5 19	syl	$⊢ φ \to W \in LMod$
21	18 4 20 7	lsatlssel	$⊢ φ \to U \in LSubSp (W)$
22	6	eldifad	$⊢ φ \to X \in V$
23	1 18 3 20 21 22	ellspsn5b	$⊢ φ \to (X \in U \leftrightarrow N (\{X\}) \subseteq U)$
24	23	adantr	$⊢ (φ \land U = N (\{X\})) \to (X \in U \leftrightarrow N (\{X\}) \subseteq U)$
25	17 24	mpbird	$⊢ (φ \land U = N (\{X\})) \to X \in U$
26	15 25	impbida	$⊢ φ \to (X \in U \leftrightarrow U = N (\{X\}))$

Metamath Proof Explorer