Theorem lsatspn0

Description: The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lsatspn0.v	$$⊢V={\mathrm{Base}}_W$$
2		lsatspn0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lsatspn0.o	$$⊢\underset{\dot{}}{0}=0_W$$
4		lsatspn0.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		isateln0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
6		isateln0.x	$$⊢\phi \to X\in V$$
7	5	adantr	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\to W\in \mathrm{LMod}$$
8		simpr	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\to N\left(\left\{X\right\}\right)\in A$$
9	3 4 7 8	lsatn0	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\to N\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}$$
10		sneq	$$⊢X=\underset{\dot{}}{0}\to \left\{X\right\}=\left\{\underset{\dot{}}{0}\right\}$$
11	10	fveq2d	$$⊢X=\underset{\dot{}}{0}\to N\left(\left\{X\right\}\right)=N\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
12	11	adantl	$$⊢\left(\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\wedge X=\underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)=N\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
13	7	adantr	$$⊢\left(\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\wedge X=\underset{\dot{}}{0}\right)\to W\in \mathrm{LMod}$$
14	3 2	lspsn0	$$⊢W\in \mathrm{LMod}\to N\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
15	13 14	syl	$$⊢\left(\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\wedge X=\underset{\dot{}}{0}\right)\to N\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
16	12 15	eqtrd	$$⊢\left(\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\wedge X=\underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
17	16	ex	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\to \left(X=\underset{\dot{}}{0}\to N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
18	17	necon3d	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\to \left(N\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\to X\ne \underset{\dot{}}{0}\right)$$
19	9 18	mpd	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\in A\right)\to X\ne \underset{\dot{}}{0}$$
20	5	adantr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to W\in \mathrm{LMod}$$
21	6	adantr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to X\in V$$
22		simpr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to X\ne \underset{\dot{}}{0}$$
23		eldifsn	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in V\wedge X\ne \underset{\dot{}}{0}\right)$$
24	21 22 23	sylanbrc	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
25	1 2 3 4 20 24	lsatlspsn	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)\in A$$
26	19 25	impbida	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\in A\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$