Theorem lsateln0

Description: A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lsateln0.z	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsateln0.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
3		lsateln0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lsateln0.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		eldifi	$$⊢v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to v\in {\mathrm{Base}}_W$$
11	5 6	lspsnid	$$⊢\left(W\in \mathrm{LMod}\wedge v\in {\mathrm{Base}}_W\right)\to v\in \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)$$
12	3 10 11	syl2an	$$⊢\left(\phi \wedge v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to v\in \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)$$
13		eleq2	$$⊢U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\to \left(v\in U\leftrightarrow v\in \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\right)$$
14	12 13	syl5ibrcom	$$⊢\left(\phi \wedge v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(U=\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\to v\in U\right)$$
15	14	reximdva	$$⊢\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 \exists v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)v\in U\right)$$
16	9 15	mpd	$$⊢\phi \to \exists v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)v\in U$$
17		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)$$
18	17	anbi1i	$$⊢\left(v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge v\in U\right)\leftrightarrow \left(\left(v\in {\mathrm{Base}}_W\wedge v\ne \underset{\dot{}}{0}\right)\wedge v\in U\right)$$
19		anass	$$⊢\left(\left(v\in {\mathrm{Base}}_W\wedge v\ne \underset{\dot{}}{0}\right)\wedge v\in U\right)\leftrightarrow \left(v\in {\mathrm{Base}}_W\wedge \left(v\ne \underset{\dot{}}{0}\wedge v\in U\right)\right)$$
20	18 19	bitri	$$⊢\left(v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge v\in U\right)\leftrightarrow \left(v\in {\mathrm{Base}}_W\wedge \left(v\ne \underset{\dot{}}{0}\wedge v\in U\right)\right)$$
21	20	simprbi	$$⊢\left(v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge v\in U\right)\to \left(v\ne \underset{\dot{}}{0}\wedge v\in U\right)$$
22	21	ancomd	$$⊢\left(v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge v\in U\right)\to \left(v\in U\wedge v\ne \underset{\dot{}}{0}\right)$$
23	22	reximi2	$$⊢\exists v\in \left({\mathrm{Base}}_W\setminus \left\{\underset{\dot{}}{0}\right\}\right)v\in U\to \exists v\in Uv\ne \underset{\dot{}}{0}$$
24	16 23	syl	$$⊢\phi \to \exists v\in Uv\ne \underset{\dot{}}{0}$$