Theorem lsatcvat2

Description: A subspace covered by the sum of two distinct atoms is an atom. ( atcvat2i analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsatcvat2.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lsatcvat2.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lsatcvat2.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatcvat2.c	$$⊢C={⋖}_L\left(W\right)$$
	lsatcvat2.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatcvat2.u	$$⊢\phi \to U\in S$$
	lsatcvat2.q	$$⊢\phi \to Q\in A$$
	lsatcvat2.r	$$⊢\phi \to R\in A$$
	lsatcvat2.n	$$⊢\phi \to Q\ne R$$
	lsatcvat2.l	$$⊢\phi \to UC\left(Q\underset{\dot{}}{\oplus }R\right)$$
Assertion	lsatcvat2	$$⊢\phi \to U\in A$$

Proof

Step	Hyp	Ref	Expression
1		lsatcvat2.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lsatcvat2.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
3		lsatcvat2.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
4		lsatcvat2.c	$$⊢C={⋖}_L\left(W\right)$$
5		lsatcvat2.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lsatcvat2.u	$$⊢\phi \to U\in S$$
7		lsatcvat2.q	$$⊢\phi \to Q\in A$$
8		lsatcvat2.r	$$⊢\phi \to R\in A$$
9		lsatcvat2.n	$$⊢\phi \to Q\ne R$$
10		lsatcvat2.l	$$⊢\phi \to UC\left(Q\underset{\dot{}}{\oplus }R\right)$$
11		eqid	$$⊢0_W=0_W$$
12	11 2 1 3 4 5 6 7 8 10	lsatcv1	$$⊢\phi \to \left(U=\left\{0_W\right\}\leftrightarrow Q=R\right)$$
13	12	necon3bid	$$⊢\phi \to \left(U\ne \left\{0_W\right\}\leftrightarrow Q\ne R\right)$$
14	9 13	mpbird	$$⊢\phi \to U\ne \left\{0_W\right\}$$
15		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
16	5 15	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
17	1 3 16 7	lsatlssel	$$⊢\phi \to Q\in S$$
18	1 3 16 8	lsatlssel	$$⊢\phi \to R\in S$$
19	1 2	lsmcl	$$⊢\left(W\in \mathrm{LMod}\wedge Q\in S\wedge R\in S\right)\to Q\underset{\dot{}}{\oplus }R\in S$$
20	16 17 18 19	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\oplus }R\in S$$
21	1 4 5 6 20 10	lcvpss	$$⊢\phi \to U\subset Q\underset{\dot{}}{\oplus }R$$
22	11 1 2 3 5 6 7 8 14 21	lsatcvat	$$⊢\phi \to U\in A$$