Theorem cdleme19a

Description: Part of proof of Lemma E in Crawley p. 113, 5th paragraph on p. 114, 1st line. D represents s_2. In their notation, we prove that if r <_ s \/ t, then s_2=(s \/ t) /\ w. (Contributed by NM, 13-Nov-2012)

	Ref	Expression
Hypotheses	cdleme19.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme19.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme19.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme19.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme19.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme19.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme19.f	$$⊢F=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme19.g	$$⊢G=\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme19.d	$$⊢D=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
	cdleme19.y	$$⊢Y=\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
Assertion	cdleme19a	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to D=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$

Proof

Step	Hyp	Ref	Expression
1		cdleme19.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme19.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme19.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdleme19.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdleme19.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdleme19.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
7		cdleme19.f	$$⊢F=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
8		cdleme19.g	$$⊢G=\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
9		cdleme19.d	$$⊢D=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
10		cdleme19.y	$$⊢Y=\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
11		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
12		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
13	12	3ad2ant1	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to K\in \mathrm{Lat}$$
14		simp1	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to K\in \mathrm{HL}$$
15		simp21	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\in A$$
16		simp22	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\in A$$
17	11 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge S\in A\right)\to R\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
18	14 15 16 17	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
19		simp23	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to T\in A$$
20	11 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge T\in A\right)\to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
21	14 16 19 20	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
22		simp33	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
23	1 2 4	hlatlej1	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge T\in A\right)\to S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
24	14 16 19 23	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
25	11 4	atbase	$$⊢R\in A\to R\in {\mathrm{Base}}_K$$
26	15 25	syl	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\in {\mathrm{Base}}_K$$
27	11 4	atbase	$$⊢S\in A\to S\in {\mathrm{Base}}_K$$
28	16 27	syl	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\in {\mathrm{Base}}_K$$
29	11 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(R\in {\mathrm{Base}}_K\wedge S\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\right)\right)\to \left(\left(R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
30	13 26 28 21 29	syl13anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
31	22 24 30	mpbi2and	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
32	1 2 4	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge S\in A\right)\to S\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
33	14 15 16 32	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
34		hlcvl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{CvLat}$$
35	34	3ad2ant1	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to K\in \mathrm{CvLat}$$
36		simp31	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
37		simp32	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
38		nbrne2	$$⊢\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to R\ne S$$
39	36 37 38	syl2anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\ne S$$
40	1 2 4	cvlatexch1	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(R\in A\wedge T\in A\wedge S\in A\right)\wedge R\ne S\right)\to \left(R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\to T\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }R\right)\right)$$
41	35 15 19 16 39 40	syl131anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\to T\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }R\right)\right)$$
42	22 41	mpd	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to T\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }R\right)$$
43	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge S\in A\right)\to R\underset{\dot{}}{\vee }S=S\underset{\dot{}}{\vee }R$$
44	14 15 16 43	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\underset{\dot{}}{\vee }S=S\underset{\dot{}}{\vee }R$$
45	42 44	breqtrrd	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to T\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
46	11 4	atbase	$$⊢T\in A\to T\in {\mathrm{Base}}_K$$
47	19 46	syl	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to T\in {\mathrm{Base}}_K$$
48	11 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(S\in {\mathrm{Base}}_K\wedge T\in {\mathrm{Base}}_K\wedge R\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\right)\right)\to \left(\left(S\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\wedge T\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\leftrightarrow \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)$$
49	13 28 47 18 48	syl13anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(S\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\wedge T\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\leftrightarrow \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)$$
50	33 45 49	mpbi2and	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
51	11 1 13 18 21 31 50	latasymd	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\underset{\dot{}}{\vee }S=S\underset{\dot{}}{\vee }T$$
52	51	oveq1d	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
53	9 52	syl5eq	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to D=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$