Theorem islsat

Description: The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	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)$$
Assertion	islsat	$$⊢W\in X\to \left(U\in A\leftrightarrow \exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)U=N\left(\left\{x\right\}\right)\right)$$

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	1 2 3 4	lsatset	$$⊢W\in X\to A=\mathrm{ran}\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼N\left(\left\{x\right\}\right)\right)$$
6	5	eleq2d	$$⊢W\in X\to \left(U\in A\leftrightarrow U\in \mathrm{ran}\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼N\left(\left\{x\right\}\right)\right)\right)$$
7		eqid	$$⊢\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼N\left(\left\{x\right\}\right)\right)=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼N\left(\left\{x\right\}\right)\right)$$
8		fvex	$$⊢N\left(\left\{x\right\}\right)\in \mathrm{V}$$
9	7 8	elrnmpti	$$⊢U\in \mathrm{ran}\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼N\left(\left\{x\right\}\right)\right)\leftrightarrow \exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)U=N\left(\left\{x\right\}\right)$$
10	6 9	bitrdi	$$⊢W\in X\to \left(U\in A\leftrightarrow \exists x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)U=N\left(\left\{x\right\}\right)\right)$$