Theorem lsatn0

Description: A 1-dim subspace (atom) of a left module or left vector space is nonzero. ( atne0 analog.) (Contributed by NM, 25-Aug-2014)

	Ref	Expression
Hypotheses	lsatn0.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatn0.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatn0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lsatn0.u	$$⊢\phi \to U\in A$$
Assertion	lsatn0	$$⊢\phi \to U\ne \left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lsatn0.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsatn0.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
3		lsatn0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lsatn0.u	$$⊢\phi \to U\in A$$
5		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
6		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
7	5 6 1 2	islsat	$$⊢W\in \mathrm{LMod}\to \left(U\in A\leftrightarrow \exists v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\right)$$
8	3 7	syl	$$⊢\phi \to \left(U\in A\leftrightarrow \exists v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\right)$$
9	4 8	mpbid	$$⊢\phi \to \exists v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)$$
10		eldifsn	$$⊢v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(v\in {\mathrm{Base}}_W\wedge v\ne \underset{\dot{}}{0}\right)$$
11	5 1 6	lspsneq0	$$⊢\left(W\in \mathrm{LMod}\wedge v\in {\mathrm{Base}}_W\right)\to \left(\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow v=\underset{\dot{}}{0}\right)$$
12	3 11	sylan	$$⊢\left(\phi \wedge v\in {\mathrm{Base}}_W\right)\to \left(\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow v=\underset{\dot{}}{0}\right)$$
13	12	biimpd	$$⊢\left(\phi \wedge v\in {\mathrm{Base}}_W\right)\to \left(\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\to v=\underset{\dot{}}{0}\right)$$
14	13	necon3d	$$⊢\left(\phi \wedge v\in {\mathrm{Base}}_W\right)\to \left(v\ne \underset{\dot{}}{0}\to \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\right)$$
15	14	expimpd	$$⊢\phi \to \left(\left(v\in {\mathrm{Base}}_W\wedge v\ne \underset{\dot{}}{0}\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\right)$$
16	10 15	syl5bi	$$⊢\phi \to \left(v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\right)$$
17		neeq1	$$⊢U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\to \left(U\ne \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\right)$$
18	17	biimprcd	$$⊢\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\to \left(U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\to U\ne \left\{\underset{\dot{}}{0}\right\}\right)$$
19	16 18	syl6	$$⊢\phi \to \left(v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \left(U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\to U\ne \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
20	19	rexlimdv	$$⊢\phi \to \left(\exists v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\to U\ne \left\{\underset{\dot{}}{0}\right\}\right)$$
21	9 20	mpd	$$⊢\phi \to U\ne \left\{\underset{\dot{}}{0}\right\}$$