Theorem lsatcvat

Description: A nonzero subspace less than the sum of two atoms is an atom. ( atcvati analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsatcvat.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatcvat.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lsatcvat.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lsatcvat.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatcvat.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatcvat.u	$$⊢\phi \to U\in S$$
	lsatcvat.q	$$⊢\phi \to Q\in A$$
	lsatcvat.r	$$⊢\phi \to R\in A$$
	lsatcvat.n	$$⊢\phi \to U\ne \left\{\underset{\dot{}}{0}\right\}$$
	lsatcvat.l	$$⊢\phi \to U\subset Q\underset{\dot{}}{\oplus }R$$
Assertion	lsatcvat	$$⊢\phi \to U\in A$$

Proof

Step	Hyp	Ref	Expression
1		lsatcvat.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsatcvat.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		lsatcvat.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
4		lsatcvat.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		lsatcvat.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lsatcvat.u	$$⊢\phi \to U\in S$$
7		lsatcvat.q	$$⊢\phi \to Q\in A$$
8		lsatcvat.r	$$⊢\phi \to R\in A$$
9		lsatcvat.n	$$⊢\phi \to U\ne \left\{\underset{\dot{}}{0}\right\}$$
10		lsatcvat.l	$$⊢\phi \to U\subset Q\underset{\dot{}}{\oplus }R$$
11	5	adantr	$$⊢\left(\phi \wedge \neg Q\subseteq U\right)\to W\in \mathrm{LVec}$$
12	6	adantr	$$⊢\left(\phi \wedge \neg Q\subseteq U\right)\to U\in S$$
13	7	adantr	$$⊢\left(\phi \wedge \neg Q\subseteq U\right)\to Q\in A$$
14	8	adantr	$$⊢\left(\phi \wedge \neg Q\subseteq U\right)\to R\in A$$
15	9	adantr	$$⊢\left(\phi \wedge \neg Q\subseteq U\right)\to U\ne \left\{\underset{\dot{}}{0}\right\}$$
16	10	adantr	$$⊢\left(\phi \wedge \neg Q\subseteq U\right)\to U\subset Q\underset{\dot{}}{\oplus }R$$
17		simpr	$$⊢\left(\phi \wedge \neg Q\subseteq U\right)\to \neg Q\subseteq U$$
18	1 2 3 4 11 12 13 14 15 16 17	lsatcvatlem	$$⊢\left(\phi \wedge \neg Q\subseteq U\right)\to U\in A$$
19	5	adantr	$$⊢\left(\phi \wedge \neg R\subseteq U\right)\to W\in \mathrm{LVec}$$
20	6	adantr	$$⊢\left(\phi \wedge \neg R\subseteq U\right)\to U\in S$$
21	8	adantr	$$⊢\left(\phi \wedge \neg R\subseteq U\right)\to R\in A$$
22	7	adantr	$$⊢\left(\phi \wedge \neg R\subseteq U\right)\to Q\in A$$
23	9	adantr	$$⊢\left(\phi \wedge \neg R\subseteq U\right)\to U\ne \left\{\underset{\dot{}}{0}\right\}$$
24		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
25	5 24	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
26		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
27	25 26	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
28	2	lsssssubg	$$⊢W\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(W\right)$$
29	25 28	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(W\right)$$
30	2 4 25 7	lsatlssel	$$⊢\phi \to Q\in S$$
31	29 30	sseldd	$$⊢\phi \to Q\in \mathrm{SubGrp}\left(W\right)$$
32	2 4 25 8	lsatlssel	$$⊢\phi \to R\in S$$
33	29 32	sseldd	$$⊢\phi \to R\in \mathrm{SubGrp}\left(W\right)$$
34	3	lsmcom	$$⊢\left(W\in \mathrm{Abel}\wedge Q\in \mathrm{SubGrp}\left(W\right)\wedge R\in \mathrm{SubGrp}\left(W\right)\right)\to Q\underset{\dot{}}{\oplus }R=R\underset{\dot{}}{\oplus }Q$$
35	27 31 33 34	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\oplus }R=R\underset{\dot{}}{\oplus }Q$$
36	35	psseq2d	$$⊢\phi \to \left(U\subset Q\underset{\dot{}}{\oplus }R\leftrightarrow U\subset R\underset{\dot{}}{\oplus }Q\right)$$
37	10 36	mpbid	$$⊢\phi \to U\subset R\underset{\dot{}}{\oplus }Q$$
38	37	adantr	$$⊢\left(\phi \wedge \neg R\subseteq U\right)\to U\subset R\underset{\dot{}}{\oplus }Q$$
39		simpr	$$⊢\left(\phi \wedge \neg R\subseteq U\right)\to \neg R\subseteq U$$
40	1 2 3 4 19 20 21 22 23 38 39	lsatcvatlem	$$⊢\left(\phi \wedge \neg R\subseteq U\right)\to U\in A$$
41	29 6	sseldd	$$⊢\phi \to U\in \mathrm{SubGrp}\left(W\right)$$
42	3	lsmlub	$$⊢\left(Q\in \mathrm{SubGrp}\left(W\right)\wedge R\in \mathrm{SubGrp}\left(W\right)\wedge U\in \mathrm{SubGrp}\left(W\right)\right)\to \left(\left(Q\subseteq U\wedge R\subseteq U\right)\leftrightarrow Q\underset{\dot{}}{\oplus }R\subseteq U\right)$$
43	31 33 41 42	syl3anc	$$⊢\phi \to \left(\left(Q\subseteq U\wedge R\subseteq U\right)\leftrightarrow Q\underset{\dot{}}{\oplus }R\subseteq U\right)$$
44		ssnpss	$$⊢Q\underset{\dot{}}{\oplus }R\subseteq U\to \neg U\subset Q\underset{\dot{}}{\oplus }R$$
45	43 44	syl6bi	$$⊢\phi \to \left(\left(Q\subseteq U\wedge R\subseteq U\right)\to \neg U\subset Q\underset{\dot{}}{\oplus }R\right)$$
46	45	con2d	$$⊢\phi \to \left(U\subset Q\underset{\dot{}}{\oplus }R\to \neg \left(Q\subseteq U\wedge R\subseteq U\right)\right)$$
47		ianor	$$⊢\neg \left(Q\subseteq U\wedge R\subseteq U\right)\leftrightarrow \left(\neg Q\subseteq U\vee \neg R\subseteq U\right)$$
48	46 47	syl6ib	$$⊢\phi \to \left(U\subset Q\underset{\dot{}}{\oplus }R\to \left(\neg Q\subseteq U\vee \neg R\subseteq U\right)\right)$$
49	10 48	mpd	$$⊢\phi \to \left(\neg Q\subseteq U\vee \neg R\subseteq U\right)$$
50	18 40 49	mpjaodan	$$⊢\phi \to U\in A$$