Theorem paddasslem2

Description: Lemma for paddass . (Contributed by NM, 8-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	paddasslem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	paddasslem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	paddasslem2	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to z\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)$$

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		paddasslem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		paddasslem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		simp1l	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to K\in \mathrm{HL}$$
5		simp1r	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to r\in A$$
6		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to z\in A$$
7		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to y\in A$$
8	5 6 7	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(r\in A\wedge z\in A\wedge y\in A\right)$$
9		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to x\in A$$
10		simp3l	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to \neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)$$
11	1 2 3	atnlej2	$$⊢\left(K\in \mathrm{HL}\wedge \left(r\in A\wedge x\in A\wedge y\in A\right)\wedge \neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\to r\ne y$$
12	4 5 9 7 10 11	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to r\ne y$$
13	4 8 12	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge \left(r\in A\wedge z\in A\wedge y\in A\right)\wedge r\ne y\right)$$
14		simp3r	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)$$
15	1 2 3	hlatexch1	$$⊢\left(K\in \mathrm{HL}\wedge \left(r\in A\wedge z\in A\wedge y\in A\right)\wedge r\ne y\right)\to \left(r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\to z\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }r\right)\right)$$
16	13 14 15	sylc	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to z\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }r\right)$$
17	4	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to K\in \mathrm{Lat}$$
18		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
19	18 3	atbase	$$⊢r\in A\to r\in {\mathrm{Base}}_K$$
20	5 19	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to r\in {\mathrm{Base}}_K$$
21	18 3	atbase	$$⊢y\in A\to y\in {\mathrm{Base}}_K$$
22	7 21	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to y\in {\mathrm{Base}}_K$$
23	18 2	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge r\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\to r\underset{\dot{}}{\vee }y=y\underset{\dot{}}{\vee }r$$
24	17 20 22 23	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to r\underset{\dot{}}{\vee }y=y\underset{\dot{}}{\vee }r$$
25	16 24	breqtrrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge r\in A\right)\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\wedge \left(\neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge r\underset{\dot{}}{\le }\left(y\underset{\dot{}}{\vee }z\right)\right)\right)\to z\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)$$