Theorem 3atlem2

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	3atlem2	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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)$$
5		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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}$$
6	5	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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}$$
7		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
8		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
9		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
10	9 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$$
11	5 7 8 10	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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	9 3	atbase	$$⊢R\in A\to R\in {\mathrm{Base}}_K$$
14	12 13	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
15		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
16		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
17	9 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$$
18	5 15 16 17	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
19		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
20	9 3	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
21	19 20	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
22	9 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$$
23	6 18 21 22	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
24	9 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)$$
25	6 11 14 23 24	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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)$$
26	4 25	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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)$$
27	26	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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)$$
28	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)$$
29	5 15 16 19 28	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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)$$
30		simp22r	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(T\underset{\dot{}}{\vee }U\right)$$
31		simp22l	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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\ne U$$
32	1 2 3	hlatexchb2	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge T\in A\wedge U\in A\right)\wedge P\ne U\right)\to \left(P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\leftrightarrow P\underset{\dot{}}{\vee }U=T\underset{\dot{}}{\vee }U\right)$$
33	5 7 16 19 31 32	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(T\underset{\dot{}}{\vee }U\right)\leftrightarrow P\underset{\dot{}}{\vee }U=T\underset{\dot{}}{\vee }U\right)$$
34	30 33	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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=T\underset{\dot{}}{\vee }U$$
35	34	oveq2d	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 }\left(P\underset{\dot{}}{\vee }U\right)=S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)$$
36	29 35	eqtr4d	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(P\underset{\dot{}}{\vee }U\right)$$
37	2 3	hlatjass	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge U\in A\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }U=P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }U\right)$$
38	5 7 8 19 37	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 }U=P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }U\right)$$
39	2 3	hlatj12	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge U\in A\right)\right)\to P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }U\right)=Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)$$
40	5 7 8 19 39	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 }U\right)=Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)$$
41	2 3	hlatj32	$$⊢\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=\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }Q$$
42	5 7 8 12 41	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }Q$$
43	4 42 29	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 }R\right)\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
44	9 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$$
45	5 7 12 44	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
46	9 3	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
47	8 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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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	9 3	atbase	$$⊢S\in A\to S\in {\mathrm{Base}}_K$$
49	15 48	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 {\mathrm{Base}}_K$$
50	9 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$$
51	5 16 19 50	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
52	9 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge S\in {\mathrm{Base}}_K\wedge T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\to S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\in {\mathrm{Base}}_K$$
53	6 49 51 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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 }\left(T\underset{\dot{}}{\vee }U\right)\in {\mathrm{Base}}_K$$
54	9 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(P\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\wedge Q\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\right)\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\right)$$
55	6 45 47 53 54	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 }R\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\wedge Q\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\right)\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\right)$$
56	43 55	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 }R\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\wedge Q\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)\right)$$
57	56	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
58	57 35	breqtrrd	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(S\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)$$
59	9 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$$
60	5 7 19 59	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$
61		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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)$$
62	9 1 2 3	hlexchb2	$$⊢\left(K\in \mathrm{HL}\wedge \left(Q\in A\wedge S\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(S\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)=S\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)$$
63	5 8 15 60 61 62	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(S\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)\leftrightarrow Q\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)=S\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)\right)$$
64	58 63	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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)=S\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)$$
65	38 40 64	3eqtrd	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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 }U=S\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }U\right)$$
66	36 65	eqtr4d	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }U$$
67	27 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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }U\right)$$
68		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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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)$$
69	9 1 2 3	hlexchb1	$$⊢\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(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }U\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }U\right)$$
70	5 12 19 11 68 69	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }U\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }U\right)$$
71	67 70	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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }U$$
72	71 66	eqtr4d	$$⊢\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 \left(P\ne U\wedge P\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\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$$