Theorem lsatexch1

Description: The atom exch1ange property. ( hlatexch1 analog.) (Contributed by NM, 14-Jan-2015)

	Ref	Expression
Hypotheses	lsatexch1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lsatexch1.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatexch1.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatexch1.u	$$⊢\phi \to Q\in A$$
	lsatexch1.q	$$⊢\phi \to R\in A$$
	lsatexch1.r	$$⊢\phi \to S\in A$$
	lsatexch1.l	$$⊢\phi \to Q\subseteq S\underset{\dot{}}{\oplus }R$$
	lsatexch1.z	$$⊢\phi \to Q\ne S$$
Assertion	lsatexch1	$$⊢\phi \to R\subseteq S\underset{\dot{}}{\oplus }Q$$

Proof

Step	Hyp	Ref	Expression
1		lsatexch1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
2		lsatexch1.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
3		lsatexch1.w	$$⊢\phi \to W\in \mathrm{LVec}$$
4		lsatexch1.u	$$⊢\phi \to Q\in A$$
5		lsatexch1.q	$$⊢\phi \to R\in A$$
6		lsatexch1.r	$$⊢\phi \to S\in A$$
7		lsatexch1.l	$$⊢\phi \to Q\subseteq S\underset{\dot{}}{\oplus }R$$
8		lsatexch1.z	$$⊢\phi \to Q\ne S$$
9		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
10		eqid	$$⊢0_W=0_W$$
11		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
12	3 11	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
13	9 2 12 6	lsatlssel	$$⊢\phi \to S\in \mathrm{LSubSp}\left(W\right)$$
14	8	necomd	$$⊢\phi \to S\ne Q$$
15	10 2 3 6 4	lsatnem0	$$⊢\phi \to \left(S\ne Q\leftrightarrow S\cap Q=\left\{0_W\right\}\right)$$
16	14 15	mpbid	$$⊢\phi \to S\cap Q=\left\{0_W\right\}$$
17	9 1 10 2 3 13 4 5 7 16	lsatexch	$$⊢\phi \to R\subseteq S\underset{\dot{}}{\oplus }Q$$