Theorem l1cvat

Description: Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in Crawley p. 112. ( 1cvrat analog.) (Contributed by NM, 11-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		l1cvat.v	$$⊢V={\mathrm{Base}}_W$$
2		l1cvat.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		l1cvat.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
4		l1cvat.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		l1cvat.c	$$⊢C={⋖}_L\left(W\right)$$
6		l1cvat.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		l1cvat.u	$$⊢\phi \to U\in S$$
8		l1cvat.q	$$⊢\phi \to Q\in A$$
9		l1cvat.r	$$⊢\phi \to R\in A$$
10		l1cvat.n	$$⊢\phi \to Q\ne R$$
11		l1cvat.l	$$⊢\phi \to UCV$$
12		l1cvat.m	$$⊢\phi \to \neg Q\subseteq U$$
13		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
14	6 13	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
15		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
16	14 15	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
17	2	lsssssubg	$$⊢W\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(W\right)$$
18	14 17	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(W\right)$$
19	2 4 14 8	lsatlssel	$$⊢\phi \to Q\in S$$
20	18 19	sseldd	$$⊢\phi \to Q\in \mathrm{SubGrp}\left(W\right)$$
21	2 4 14 9	lsatlssel	$$⊢\phi \to R\in S$$
22	18 21	sseldd	$$⊢\phi \to R\in \mathrm{SubGrp}\left(W\right)$$
23	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$$
24	16 20 22 23	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\oplus }R=R\underset{\dot{}}{\oplus }Q$$
25	24	ineq1d	$$⊢\phi \to \left(Q\underset{\dot{}}{\oplus }R\right)\cap U=\left(R\underset{\dot{}}{\oplus }Q\right)\cap U$$
26		incom	$$⊢\left(R\underset{\dot{}}{\oplus }Q\right)\cap U=U\cap \left(R\underset{\dot{}}{\oplus }Q\right)$$
27	25 26	syl6eq	$$⊢\phi \to \left(Q\underset{\dot{}}{\oplus }R\right)\cap U=U\cap \left(R\underset{\dot{}}{\oplus }Q\right)$$
28	10	necomd	$$⊢\phi \to R\ne Q$$
29	1 4 14 9	lsatssv	$$⊢\phi \to R\subseteq V$$
30	1 2 3 4 5 6 7 8 11 12	l1cvpat	$$⊢\phi \to U\underset{\dot{}}{\oplus }Q=V$$
31	29 30	sseqtrrd	$$⊢\phi \to R\subseteq U\underset{\dot{}}{\oplus }Q$$
32	2 3 4 6 7 9 8 28 12 31	lsatcvat3	$$⊢\phi \to U\cap \left(R\underset{\dot{}}{\oplus }Q\right)\in A$$
33	27 32	eqeltrd	$$⊢\phi \to \left(Q\underset{\dot{}}{\oplus }R\right)\cap U\in A$$