Theorem lsatel

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

	Ref	Expression
Hypotheses	lsatel.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatel.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lsatel.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatel.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatel.u	$$⊢\phi \to U\in A$$
	lsatel.x	$$⊢\phi \to X\in U$$
	lsatel.e	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
Assertion	lsatel	$$⊢\phi \to U=N\left(\left\{X\right\}\right)$$

Proof

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