Theorem lsatelbN

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lsatelb.v	$$⊢V={\mathrm{Base}}_W$$
	lsatelb.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatelb.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lsatelb.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatelb.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatelb.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lsatelb.u	$$⊢\phi \to U\in A$$
Assertion	lsatelbN	$$⊢\phi \to \left(X\in U\leftrightarrow U=N\left(\left\{X\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsatelb.v	$$⊢V={\mathrm{Base}}_W$$
2		lsatelb.o	$$⊢\underset{\dot{}}{0}=0_W$$
3		lsatelb.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lsatelb.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		lsatelb.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lsatelb.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		lsatelb.u	$$⊢\phi \to U\in A$$
8	5	adantr	$$⊢\left(\phi \wedge X\in U\right)\to W\in \mathrm{LVec}$$
9	7	adantr	$$⊢\left(\phi \wedge X\in U\right)\to U\in A$$
10		simpr	$$⊢\left(\phi \wedge X\in U\right)\to X\in U$$
11		eldifsn	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in V\wedge X\ne \underset{\dot{}}{0}\right)$$
12	6 11	sylib	$$⊢\phi \to \left(X\in V\wedge X\ne \underset{\dot{}}{0}\right)$$
13	12	simprd	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
14	13	adantr	$$⊢\left(\phi \wedge X\in U\right)\to X\ne \underset{\dot{}}{0}$$
15	2 3 4 8 9 10 14	lsatel	$$⊢\left(\phi \wedge X\in U\right)\to U=N\left(\left\{X\right\}\right)$$
16		eqimss2	$$⊢U=N\left(\left\{X\right\}\right)\to N\left(\left\{X\right\}\right)\subseteq U$$
17	16	adantl	$$⊢\left(\phi \wedge U=N\left(\left\{X\right\}\right)\right)\to N\left(\left\{X\right\}\right)\subseteq U$$
18		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
19		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
20	5 19	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
21	18 4 20 7	lsatlssel	$$⊢\phi \to U\in \mathrm{LSubSp}\left(W\right)$$
22	6	eldifad	$$⊢\phi \to X\in V$$
23	1 18 3 20 21 22	ellspsn5b	$$⊢\phi \to \left(X\in U\leftrightarrow N\left(\left\{X\right\}\right)\subseteq U\right)$$
24	23	adantr	$$⊢\left(\phi \wedge U=N\left(\left\{X\right\}\right)\right)\to \left(X\in U\leftrightarrow N\left(\left\{X\right\}\right)\subseteq U\right)$$
25	17 24	mpbird	$$⊢\left(\phi \wedge U=N\left(\left\{X\right\}\right)\right)\to X\in U$$
26	15 25	impbida	$$⊢\phi \to \left(X\in U\leftrightarrow U=N\left(\left\{X\right\}\right)\right)$$