Theorem cdleme3

Description: Part of proof of Lemma E in Crawley p. 113. F represents f(r). W is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa above, we show that f(r) e. W (4th line from bottom on p. 113), meaning it is an atom and not under w, which in our notation is expressed as F e. A /\ -. F .<_ W . Their proof provides no details of our lemmas cdleme3b through cdleme3 , so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012)

	Ref	Expression
Hypotheses	cdleme1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme1.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme1.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme1.f	$$⊢F=\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme3	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \neg F\underset{\dot{}}{\le }W$$

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme1.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdleme1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdleme1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdleme1.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
7		cdleme1.f	$$⊢F=\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
8		eqid	$$⊢\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W=\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W$$
9	1 2 3 4 5 6 7 8	cdleme3g	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to F\ne U$$
10		simp1l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to K\in \mathrm{HL}$$
11	10	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to K\in \mathrm{Lat}$$
12		simp23l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to R\in A$$
13		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
14	13 4	atbase	$$⊢R\in A\to R\in {\mathrm{Base}}_K$$
15	12 14	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to R\in {\mathrm{Base}}_K$$
16	1 2 3 4 5 6 7	cdleme3fa	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to F\in A$$
17	13 4	atbase	$$⊢F\in A\to F\in {\mathrm{Base}}_K$$
18	16 17	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to F\in {\mathrm{Base}}_K$$
19	13 1 2	latlej2	$$⊢\left(K\in \mathrm{Lat}\wedge R\in {\mathrm{Base}}_K\wedge F\in {\mathrm{Base}}_K\right)\to F\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }F\right)$$
20	11 15 18 19	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to F\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }F\right)$$
21	20	biantrurd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(F\underset{\dot{}}{\le }W\leftrightarrow \left(F\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }F\right)\wedge F\underset{\dot{}}{\le }W\right)\right)$$
22	13 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge F\in A\right)\to R\underset{\dot{}}{\vee }F\in {\mathrm{Base}}_K$$
23	10 12 16 22	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to R\underset{\dot{}}{\vee }F\in {\mathrm{Base}}_K$$
24		simp1r	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to W\in H$$
25	13 5	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
26	24 25	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to W\in {\mathrm{Base}}_K$$
27	13 1 3	latlem12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(F\in {\mathrm{Base}}_K\wedge R\underset{\dot{}}{\vee }F\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(F\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }F\right)\wedge F\underset{\dot{}}{\le }W\right)\leftrightarrow F\underset{\dot{}}{\le }\left(\left(R\underset{\dot{}}{\vee }F\right)\underset{\dot{}}{\wedge }W\right)\right)$$
28	11 18 23 26 27	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(\left(F\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }F\right)\wedge F\underset{\dot{}}{\le }W\right)\leftrightarrow F\underset{\dot{}}{\le }\left(\left(R\underset{\dot{}}{\vee }F\right)\underset{\dot{}}{\wedge }W\right)\right)$$
29		simp1	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
30		simp21l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to P\in A$$
31		simp22l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to Q\in A$$
32		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)$$
33	1 2 3 4 5 6 7	cdleme2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\right)\to \left(R\underset{\dot{}}{\vee }F\right)\underset{\dot{}}{\wedge }W=U$$
34	29 30 31 32 33	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(R\underset{\dot{}}{\vee }F\right)\underset{\dot{}}{\wedge }W=U$$
35	34	breq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(F\underset{\dot{}}{\le }\left(\left(R\underset{\dot{}}{\vee }F\right)\underset{\dot{}}{\wedge }W\right)\leftrightarrow F\underset{\dot{}}{\le }U\right)$$
36	28 35	bitrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(\left(F\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }F\right)\wedge F\underset{\dot{}}{\le }W\right)\leftrightarrow F\underset{\dot{}}{\le }U\right)$$
37		hlatl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{AtLat}$$
38	10 37	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to K\in \mathrm{AtLat}$$
39		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
40		simp3l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to P\ne Q$$
41	1 2 3 4 5 6	lhpat2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge P\ne Q\right)\right)\to U\in A$$
42	29 39 31 40 41	syl112anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to U\in A$$
43	1 4	atcmp	$$⊢\left(K\in \mathrm{AtLat}\wedge F\in A\wedge U\in A\right)\to \left(F\underset{\dot{}}{\le }U\leftrightarrow F=U\right)$$
44	38 16 42 43	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(F\underset{\dot{}}{\le }U\leftrightarrow F=U\right)$$
45	21 36 44	3bitrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(F\underset{\dot{}}{\le }W\leftrightarrow F=U\right)$$
46	45	necon3bbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(\neg F\underset{\dot{}}{\le }W\leftrightarrow F\ne U\right)$$
47	9 46	mpbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \neg F\underset{\dot{}}{\le }W$$