lsatel

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014)

Step	Hyp	Ref	Expression
1		lsatel.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lsatel.n	$⊢ N = LSpan (W)$
3		lsatel.a	$⊢ A = LSAtoms (W)$
4		lsatel.w	$⊢ φ \to W \in LVec$
5		lsatel.u	$⊢ φ \to U \in A$
6		lsatel.x	$⊢ φ \to X \in U$
7		lsatel.e	$⊢ φ \to X \neq \underset{˙}{0}$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	4 9	syl	$⊢ φ \to W \in LMod$
11	8 3 10 5	lsatlssel	$⊢ φ \to U \in LSubSp (W)$
12	8 2 10 11 6	ellspsn5	$⊢ φ \to N (\{X\}) \subseteq U$
13		eqid	$⊢ {Base}_{W} = {Base}_{W}$
14	13 8	lssel	$⊢ (U \in LSubSp (W) \land X \in U) \to X \in {Base}_{W}$
15	11 6 14	syl2anc	$⊢ φ \to X \in {Base}_{W}$
16	13 2 1 3	lsatlspsn2	$⊢ (W \in LMod \land X \in {Base}_{W} \land X \neq \underset{˙}{0}) \to N (\{X\}) \in A$
17	10 15 7 16	syl3anc	$⊢ φ \to N (\{X\}) \in A$
18	3 4 17 5	lsatcmp	$⊢ φ \to (N (\{X\}) \subseteq U \leftrightarrow N (\{X\}) = U)$
19	12 18	mpbid	$⊢ φ \to N (\{X\}) = U$
20	19	eqcomd	$⊢ φ \to U = N (\{X\})$

Metamath Proof Explorer