Theorem lsatcvat3

Description: A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. ( atcvat3i analog.) (Contributed by NM, 11-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lsatcvat3.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lsatcvat3.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
3		lsatcvat3.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
4		lsatcvat3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
5		lsatcvat3.u	$$⊢\phi \to U\in S$$
6		lsatcvat3.q	$$⊢\phi \to Q\in A$$
7		lsatcvat3.r	$$⊢\phi \to R\in A$$
8		lsatcvat3.n	$$⊢\phi \to Q\ne R$$
9		lsatcvat3.m	$$⊢\phi \to \neg R\subseteq U$$
10		lsatcvat3.l	$$⊢\phi \to Q\subseteq U\underset{\dot{}}{\oplus }R$$
11		eqid	$$⊢{⋖}_L\left(W\right)={⋖}_L\left(W\right)$$
12		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
13	4 12	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
14	1 3 13 6	lsatlssel	$$⊢\phi \to Q\in S$$
15	1 3 13 7	lsatlssel	$$⊢\phi \to R\in S$$
16	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$$
17	13 14 15 16	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\oplus }R\in S$$
18	1	lssincl	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\wedge Q\underset{\dot{}}{\oplus }R\in S\right)\to U\cap \left(Q\underset{\dot{}}{\oplus }R\right)\in S$$
19	13 5 17 18	syl3anc	$$⊢\phi \to U\cap \left(Q\underset{\dot{}}{\oplus }R\right)\in S$$
20	1 2 3 11 4 5 7	lcv1	$$⊢\phi \to \left(\neg R\subseteq U\leftrightarrow U{⋖}_L\left(W\right)\left(U\underset{\dot{}}{\oplus }R\right)\right)$$
21	9 20	mpbid	$$⊢\phi \to U{⋖}_L\left(W\right)\left(U\underset{\dot{}}{\oplus }R\right)$$
22		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
23	13 22	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
24	1	lsssssubg	$$⊢W\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(W\right)$$
25	13 24	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(W\right)$$
26	25 14	sseldd	$$⊢\phi \to Q\in \mathrm{SubGrp}\left(W\right)$$
27	25 15	sseldd	$$⊢\phi \to R\in \mathrm{SubGrp}\left(W\right)$$
28	2	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$$
29	23 26 27 28	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\oplus }R=R\underset{\dot{}}{\oplus }Q$$
30	29	oveq2d	$$⊢\phi \to U\underset{\dot{}}{\oplus }\left(Q\underset{\dot{}}{\oplus }R\right)=U\underset{\dot{}}{\oplus }\left(R\underset{\dot{}}{\oplus }Q\right)$$
31	25 5	sseldd	$$⊢\phi \to U\in \mathrm{SubGrp}\left(W\right)$$
32	2	lsmass	$$⊢\left(U\in \mathrm{SubGrp}\left(W\right)\wedge R\in \mathrm{SubGrp}\left(W\right)\wedge Q\in \mathrm{SubGrp}\left(W\right)\right)\to \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }Q=U\underset{\dot{}}{\oplus }\left(R\underset{\dot{}}{\oplus }Q\right)$$
33	31 27 26 32	syl3anc	$$⊢\phi \to \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }Q=U\underset{\dot{}}{\oplus }\left(R\underset{\dot{}}{\oplus }Q\right)$$
34	30 33	eqtr4d	$$⊢\phi \to U\underset{\dot{}}{\oplus }\left(Q\underset{\dot{}}{\oplus }R\right)=\left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }Q$$
35	1 2	lsmcl	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\wedge R\in S\right)\to U\underset{\dot{}}{\oplus }R\in S$$
36	13 5 15 35	syl3anc	$$⊢\phi \to U\underset{\dot{}}{\oplus }R\in S$$
37	25 36	sseldd	$$⊢\phi \to U\underset{\dot{}}{\oplus }R\in \mathrm{SubGrp}\left(W\right)$$
38	2	lsmless2	$$⊢\left(U\underset{\dot{}}{\oplus }R\in \mathrm{SubGrp}\left(W\right)\wedge U\underset{\dot{}}{\oplus }R\in \mathrm{SubGrp}\left(W\right)\wedge Q\subseteq U\underset{\dot{}}{\oplus }R\right)\to \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }Q\subseteq \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }\left(U\underset{\dot{}}{\oplus }R\right)$$
39	37 37 10 38	syl3anc	$$⊢\phi \to \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }Q\subseteq \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }\left(U\underset{\dot{}}{\oplus }R\right)$$
40	34 39	eqsstrd	$$⊢\phi \to U\underset{\dot{}}{\oplus }\left(Q\underset{\dot{}}{\oplus }R\right)\subseteq \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }\left(U\underset{\dot{}}{\oplus }R\right)$$
41	2	lsmidm	$$⊢U\underset{\dot{}}{\oplus }R\in \mathrm{SubGrp}\left(W\right)\to \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }\left(U\underset{\dot{}}{\oplus }R\right)=U\underset{\dot{}}{\oplus }R$$
42	37 41	syl	$$⊢\phi \to \left(U\underset{\dot{}}{\oplus }R\right)\underset{\dot{}}{\oplus }\left(U\underset{\dot{}}{\oplus }R\right)=U\underset{\dot{}}{\oplus }R$$
43	40 42	sseqtrd	$$⊢\phi \to U\underset{\dot{}}{\oplus }\left(Q\underset{\dot{}}{\oplus }R\right)\subseteq U\underset{\dot{}}{\oplus }R$$
44	25 17	sseldd	$$⊢\phi \to Q\underset{\dot{}}{\oplus }R\in \mathrm{SubGrp}\left(W\right)$$
45	2	lsmub2	$$⊢\left(Q\in \mathrm{SubGrp}\left(W\right)\wedge R\in \mathrm{SubGrp}\left(W\right)\right)\to R\subseteq Q\underset{\dot{}}{\oplus }R$$
46	26 27 45	syl2anc	$$⊢\phi \to R\subseteq Q\underset{\dot{}}{\oplus }R$$
47	2	lsmless2	$$⊢\left(U\in \mathrm{SubGrp}\left(W\right)\wedge Q\underset{\dot{}}{\oplus }R\in \mathrm{SubGrp}\left(W\right)\wedge R\subseteq Q\underset{\dot{}}{\oplus }R\right)\to U\underset{\dot{}}{\oplus }R\subseteq U\underset{\dot{}}{\oplus }\left(Q\underset{\dot{}}{\oplus }R\right)$$
48	31 44 46 47	syl3anc	$$⊢\phi \to U\underset{\dot{}}{\oplus }R\subseteq U\underset{\dot{}}{\oplus }\left(Q\underset{\dot{}}{\oplus }R\right)$$
49	43 48	eqssd	$$⊢\phi \to U\underset{\dot{}}{\oplus }\left(Q\underset{\dot{}}{\oplus }R\right)=U\underset{\dot{}}{\oplus }R$$
50	21 49	breqtrrd	$$⊢\phi \to U{⋖}_L\left(W\right)\left(U\underset{\dot{}}{\oplus }\left(Q\underset{\dot{}}{\oplus }R\right)\right)$$
51	1 2 11 13 5 17 50	lcvexchlem4	$$⊢\phi \to \left(U\cap \left(Q\underset{\dot{}}{\oplus }R\right)\right){⋖}_L\left(W\right)\left(Q\underset{\dot{}}{\oplus }R\right)$$
52	1 2 3 11 4 19 6 7 8 51	lsatcvat2	$$⊢\phi \to U\cap \left(Q\underset{\dot{}}{\oplus }R\right)\in A$$