Theorem cdleme0nex

Description: Part of proof of Lemma E in Crawley p. 114, 4th line of 4th paragraph. Whenever (in their terminology) p \/ q/0 (i.e. the sublattice from 0 to p \/ q) contains precisely three atoms, any atom not under w must equal either p or q. (In case of 3 atoms, one of them must be u - see cdleme0a - which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 , our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) . Thus, the negated existential condition states there are no atoms different from p or q that are also not under w. (Contributed by NM, 12-Nov-2012)

	Ref	Expression
Hypotheses	cdleme0nex.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme0nex.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme0nex.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	cdleme0nex	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \left(R=P\vee R=Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdleme0nex.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme0nex.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme0nex.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		simp3r	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \neg R\underset{\dot{}}{\le }W$$
5		simp12	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
6	4 5	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
7		simp3l	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to R\in A$$
8		simp13	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
9		ralnex	$$⊢\forall r\in A\neg \left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\leftrightarrow \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
10	8 9	sylibr	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \forall r\in A\neg \left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
11		breq1	$$⊢r=R\to \left(r\underset{\dot{}}{\le }W\leftrightarrow R\underset{\dot{}}{\le }W\right)$$
12	11	notbid	$$⊢r=R\to \left(\neg r\underset{\dot{}}{\le }W\leftrightarrow \neg R\underset{\dot{}}{\le }W\right)$$
13		oveq2	$$⊢r=R\to P\underset{\dot{}}{\vee }r=P\underset{\dot{}}{\vee }R$$
14		oveq2	$$⊢r=R\to Q\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }R$$
15	13 14	eqeq12d	$$⊢r=R\to \left(P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\leftrightarrow P\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R\right)$$
16	12 15	anbi12d	$$⊢r=R\to \left(\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\leftrightarrow \left(\neg R\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R\right)\right)$$
17	16	notbid	$$⊢r=R\to \left(\neg \left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\leftrightarrow \neg \left(\neg R\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R\right)\right)$$
18	17	rspcva	$$⊢\left(R\in A\wedge \forall r\in A\neg \left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\to \neg \left(\neg R\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R\right)$$
19	7 10 18	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \neg \left(\neg R\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R\right)$$
20		simp11	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to K\in \mathrm{HL}$$
21		hlcvl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{CvLat}$$
22	20 21	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to K\in \mathrm{CvLat}$$
23		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to P\in A$$
24		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to Q\in A$$
25		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to P\ne Q$$
26	3 1 2	cvlsupr2	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge P\ne Q\right)\to \left(P\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R\leftrightarrow \left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
27	22 23 24 7 25 26	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \left(P\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R\leftrightarrow \left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
28	27	anbi2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \left(\left(\neg R\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R\right)\leftrightarrow \left(\neg R\underset{\dot{}}{\le }W\wedge \left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)$$
29	19 28	mtbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \neg \left(\neg R\underset{\dot{}}{\le }W\wedge \left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
30		ianor	$$⊢\neg \left(\left(R\ne P\wedge R\ne Q\right)\wedge \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\leftrightarrow \left(\neg \left(R\ne P\wedge R\ne Q\right)\vee \neg \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
31		df-3an	$$⊢\left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(\left(R\ne P\wedge R\ne Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
32	31	anbi2i	$$⊢\left(\neg R\underset{\dot{}}{\le }W\wedge \left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\leftrightarrow \left(\neg R\underset{\dot{}}{\le }W\wedge \left(\left(R\ne P\wedge R\ne Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
33		an12	$$⊢\left(\neg R\underset{\dot{}}{\le }W\wedge \left(\left(R\ne P\wedge R\ne Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\leftrightarrow \left(\left(R\ne P\wedge R\ne Q\right)\wedge \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
34	32 33	bitri	$$⊢\left(\neg R\underset{\dot{}}{\le }W\wedge \left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\leftrightarrow \left(\left(R\ne P\wedge R\ne Q\right)\wedge \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
35	34	notbii	$$⊢\neg \left(\neg R\underset{\dot{}}{\le }W\wedge \left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\leftrightarrow \neg \left(\left(R\ne P\wedge R\ne Q\right)\wedge \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
36		pm4.62	$$⊢\left(\left(R\ne P\wedge R\ne Q\right)\to \neg \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\leftrightarrow \left(\neg \left(R\ne P\wedge R\ne Q\right)\vee \neg \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
37	30 35 36	3bitr4ri	$$⊢\left(\left(R\ne P\wedge R\ne Q\right)\to \neg \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\leftrightarrow \neg \left(\neg R\underset{\dot{}}{\le }W\wedge \left(R\ne P\wedge R\ne Q\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
38	29 37	sylibr	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \left(\left(R\ne P\wedge R\ne Q\right)\to \neg \left(\neg R\underset{\dot{}}{\le }W\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
39	6 38	mt2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \neg \left(R\ne P\wedge R\ne Q\right)$$
40		neanior	$$⊢\left(R\ne P\wedge R\ne Q\right)\leftrightarrow \neg \left(R=P\vee R=Q\right)$$
41	40	con2bii	$$⊢\left(R=P\vee R=Q\right)\leftrightarrow \neg \left(R\ne P\wedge R\ne Q\right)$$
42	39 41	sylibr	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \left(R=P\vee R=Q\right)$$