Theorem lsat2el

Description: Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015)

	Ref	Expression
Hypotheses	lsat2el.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsat2el.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsat2el.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsat2el.p	$$⊢\phi \to P\in A$$
	lsat2el.q	$$⊢\phi \to Q\in A$$
	lsat2el.x	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
	lsat2el.x1	$$⊢\phi \to X\in P$$
	lsat2el.x2	$$⊢\phi \to X\in Q$$
Assertion	lsat2el	$$⊢\phi \to P=Q$$

Proof

Step	Hyp	Ref	Expression
1		lsat2el.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsat2el.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
3		lsat2el.w	$$⊢\phi \to W\in \mathrm{LVec}$$
4		lsat2el.p	$$⊢\phi \to P\in A$$
5		lsat2el.q	$$⊢\phi \to Q\in A$$
6		lsat2el.x	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
7		lsat2el.x1	$$⊢\phi \to X\in P$$
8		lsat2el.x2	$$⊢\phi \to X\in Q$$
9		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
10	1 9 2 3 4 7 6	lsatel	$$⊢\phi \to P=\mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\right)$$
11	1 9 2 3 5 8 6	lsatel	$$⊢\phi \to Q=\mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\right)$$
12	10 11	eqtr4d	$$⊢\phi \to P=Q$$