Theorem 3atlem1

Description: Lemma for 3at . (Contributed by NM, 22-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		3at.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		3at.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		3at.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		simp11	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to K\in \mathrm{HL}$$
5		simp131	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\in A$$
6		simp132	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\in A$$
7		simp133	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to U\in A$$
8	2 3	hlatjass	$$⊢\left(K\in \mathrm{HL}\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)$$
9	4 5 6 7 8	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)$$
10		simp121	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\in A$$
11		simp122	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to Q\in A$$
12		simp123	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to R\in A$$
13	2 3	hlatjass	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)$$
14	4 10 11 12 13	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)$$
15		simp3	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
16	14 15	eqbrtrrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
17	4	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to K\in \mathrm{Lat}$$
18		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
19	18 3	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
20	10 19	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\in {\mathrm{Base}}_K$$
21	18 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge R\in A\right)\to Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
22	4 11 12 21	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
23	18 2 3	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$$
24	4 5 6 23	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
25	18 3	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
26	7 25	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to U\in {\mathrm{Base}}_K$$
27	18 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
28	17 24 26 27	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
29	18 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(P\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\right)\to \left(\left(P\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\wedge \left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
30	17 20 22 28 29	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(P\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\wedge \left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
31	16 30	mpbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(P\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\wedge \left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
32	31	simpld	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
33	32 9	breqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
34	18 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge T\in A\wedge U\in A\right)\to T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
35	4 6 7 34	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
36		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)$$
37	18 1 2 3	hlexchb2	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge S\in A\wedge T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\right)\to \left(P\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow P\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)=S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
38	4 10 5 35 36 37	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(P\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow P\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)=S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
39	33 38	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)=S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)$$
40	2 3	hlatj12	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge T\in A\wedge U\in A\right)\right)\to P\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)=T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)$$
41	4 10 6 7 40	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)=T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)$$
42	9 39 41	3eqtr2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)$$
43	2 3	hlatj12	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)=Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }R\right)$$
44	4 10 11 12 43	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)=Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }R\right)$$
45	16 44 42	3brtr3d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)$$
46	18 3	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
47	11 46	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to Q\in {\mathrm{Base}}_K$$
48	18 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge R\in A\right)\to P\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
49	4 10 12 48	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
50	18 3	atbase	$$⊢T\in A\to T\in {\mathrm{Base}}_K$$
51	6 50	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\in {\mathrm{Base}}_K$$
52	18 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge U\in A\right)\to P\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
53	4 10 7 52	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
54	18 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge T\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\to T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\in {\mathrm{Base}}_K$$
55	17 51 53 54	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\in {\mathrm{Base}}_K$$
56	18 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(Q\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\in {\mathrm{Base}}_K\right)\right)\to \left(\left(Q\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\right)$$
57	17 47 49 55 56	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(Q\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\right)$$
58	45 57	mpbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(Q\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\right)$$
59	58	simpld	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to Q\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)$$
60		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)$$
61	18 1 2 3	hlexchb2	$$⊢\left(K\in \mathrm{HL}\wedge \left(Q\in A\wedge T\in A\wedge P\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\to \left(Q\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)=T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)$$
62	4 11 6 53 60 61	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(Q\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)=T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)$$
63	59 62	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)=T\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)$$
64	18 2	latj13	$$⊢\left(K\in \mathrm{Lat}\wedge \left(Q\in {\mathrm{Base}}_K\wedge P\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\right)\right)\to Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)=U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)$$
65	17 47 20 26 64	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)=U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)$$
66	42 63 65	3eqtr2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)$$
67	18 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
68	4 10 11 67	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
69	18 3	atbase	$$⊢R\in A\to R\in {\mathrm{Base}}_K$$
70	12 69	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to R\in {\mathrm{Base}}_K$$
71	18 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge R\in {\mathrm{Base}}_K\wedge \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\wedge R\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
72	17 68 70 28 71	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\wedge R\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
73	15 72	mpbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\wedge R\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
74	73	simprd	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to R\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
75	74 66	breqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to R\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
76		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
77	18 1 2 3	hlexchb2	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge U\in A\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \left(R\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow R\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)=U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
78	4 12 7 68 76 77	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(R\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow R\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)=U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
79	75 78	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to R\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)=U\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)$$
80	18 2	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge R\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\to R\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
81	17 70 68 80	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to R\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
82	66 79 81	3eqtr2rd	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }U\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$