Theorem 4atlem3b

Description: Lemma for 4at . Break inequality into 2 cases. (Contributed by NM, 9-Jul-2012)

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

Proof

Step	Hyp	Ref	Expression
1		4at.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		4at.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		4at.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		simp1	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
5		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to R\in A$$
6		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to S\in A$$
7	5 6	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(R\in A\wedge S\in A\right)$$
8		simp13	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to Q\in A$$
9		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to V\in A$$
10	8 9	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(Q\in A\wedge V\in A\right)$$
11		simp3	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
12	1 2 3	4atlem3a	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \left(Q\in A\wedge V\in A\right)\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(\neg Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)$$
13	4 7 10 11 12	syl31anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(\neg Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)$$
14		3orass	$$⊢\left(\neg Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)\leftrightarrow \left(\neg Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \left(\neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)\right)$$
15	13 14	sylib	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(\neg Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \left(\neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)\right)$$
16		simp11	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to K\in \mathrm{HL}$$
17	16	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to K\in \mathrm{Lat}$$
18		simp12	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to P\in A$$
19		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
20	19 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge V\in A\right)\to P\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K$$
21	16 18 9 20	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to P\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K$$
22	19 3	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
23	8 22	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to Q\in {\mathrm{Base}}_K$$
24	19 1 2	latlej2	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\right)\to Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\vee }Q\right)$$
25	17 21 23 24	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\vee }Q\right)$$
26	2 3	hlatj32	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge V\in A\wedge Q\in A\right)\right)\to \left(P\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\vee }Q=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V$$
27	16 18 9 8 26	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\vee }Q=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V$$
28	25 27	breqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)$$
29		biortn	$$⊢Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\to \left(\left(\neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)\leftrightarrow \left(\neg Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \left(\neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)\right)\right)$$
30	28 29	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(\left(\neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)\leftrightarrow \left(\neg Q\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \left(\neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)\right)\right)$$
31	15 30	mpbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge V\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(\neg R\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\vee \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }V\right)\right)$$