Theorem lsatlspsn

Description: The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015)

	Ref	Expression
Hypotheses	lsatset.v	$$⊢V={\mathrm{Base}}_W$$
	lsatset.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lsatset.z	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatset.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatlspsn.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lsatlspsn.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	lsatlspsn	$$⊢\phi \to N\left(\left\{X\right\}\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		lsatset.v	$$⊢V={\mathrm{Base}}_W$$
2		lsatset.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lsatset.z	$$⊢\underset{\dot{}}{0}=0_W$$
4		lsatset.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		lsatlspsn.w	$$⊢\phi \to W\in \mathrm{LMod}$$
6		lsatlspsn.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		eqid	$$⊢N\left(\left\{X\right\}\right)=N\left(\left\{X\right\}\right)$$
8		sneq	$$⊢v=X\to \left\{v\right\}=\left\{X\right\}$$
9	8	fveq2d	$$⊢v=X\to N\left(\left\{v\right\}\right)=N\left(\left\{X\right\}\right)$$
10	9	rspceeqv	$$⊢\left(X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge N\left(\left\{X\right\}\right)=N\left(\left\{X\right\}\right)\right)\to \exists v\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)N\left(\left\{X\right\}\right)=N\left(\left\{v\right\}\right)$$
11	6 7 10	sylancl	$$⊢\phi \to \exists v\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)N\left(\left\{X\right\}\right)=N\left(\left\{v\right\}\right)$$
12	1 2 3 4	islsat	$$⊢W\in \mathrm{LMod}\to \left(N\left(\left\{X\right\}\right)\in A\leftrightarrow \exists v\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)N\left(\left\{X\right\}\right)=N\left(\left\{v\right\}\right)\right)$$
13	5 12	syl	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\in A\leftrightarrow \exists v\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)N\left(\left\{X\right\}\right)=N\left(\left\{v\right\}\right)\right)$$
14	11 13	mpbird	$$⊢\phi \to N\left(\left\{X\right\}\right)\in A$$