Theorem cdleme22eALTN

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 4th line on p. 115. F , N , O represent f(z), f_z(s), f_z(t) respectively. When t \/ v = p \/ q, f_z(s) <_ f_z(t) \/ v. (Contributed by NM, 6-Dec-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme22.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme22.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme22.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme22.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme22.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme22eALT.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme22eALT.f	$$⊢F=\left(y\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme22eALT.g	$$⊢G=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme22eALT.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme22eALT.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme22eALTN	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to N\underset{\dot{}}{\le }\left(O\underset{\dot{}}{\vee }V\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdleme22.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme22.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme22.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdleme22.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdleme22.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdleme22eALT.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
7		cdleme22eALT.f	$$⊢F=\left(y\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\right)$$
8		cdleme22eALT.g	$$⊢G=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
9		cdleme22eALT.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\right)$$
10		cdleme22eALT.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
11		simp11	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to K\in \mathrm{HL}$$
12	11	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to K\in \mathrm{Lat}$$
13		simp21l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\in A$$
14		simp22l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to Q\in A$$
15		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
16	15 2 4	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$$
17	11 13 14 16	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
18		simp12	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to W\in H$$
19		simp3ll	$$⊢\left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\to y\in A$$
20	19	3ad2ant3	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to y\in A$$
21	1 2 3 4 5 6 7 15	cdleme1b	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\wedge y\in A\right)\right)\to F\in {\mathrm{Base}}_K$$
22	11 18 13 14 20 21	syl23anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to F\in {\mathrm{Base}}_K$$
23		simp31	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to S\in A$$
24	15 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge y\in A\right)\to S\underset{\dot{}}{\vee }y\in {\mathrm{Base}}_K$$
25	11 23 20 24	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to S\underset{\dot{}}{\vee }y\in {\mathrm{Base}}_K$$
26	15 5	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
27	18 26	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to W\in {\mathrm{Base}}_K$$
28	15 3	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge S\underset{\dot{}}{\vee }y\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\to \left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K$$
29	12 25 27 28	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K$$
30	15 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge F\in {\mathrm{Base}}_K\wedge \left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K\right)\to F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K$$
31	12 22 29 30	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K$$
32	15 1 3	latmle1	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
33	12 17 31 32	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }y\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
34	9 33	eqbrtrid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to N\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
35		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
36		simp13	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to T\in A$$
37		simp321	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to V\in A$$
38		simp322	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to V\underset{\dot{}}{\le }W$$
39	37 38	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
40		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\ne Q$$
41		simp323	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q$$
42	1 2 3 4 5 6	cdleme22a	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge Q\in A\wedge T\in A\right)\wedge \left(\left(V\in A\wedge V\underset{\dot{}}{\le }W\right)\wedge P\ne Q\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to V=U$$
43	11 18 35 14 36 39 40 41 42	syl233anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to V=U$$
44	43	oveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to O\underset{\dot{}}{\vee }V=O\underset{\dot{}}{\vee }U$$
45	10	oveq1i	$$⊢O\underset{\dot{}}{\vee }U=\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }U$$
46		simp21r	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \neg P\underset{\dot{}}{\le }W$$
47	1 2 3 4 5 6	cdleme0a	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge P\ne Q\right)\right)\to U\in A$$
48	11 18 13 46 14 40 47	syl222anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to U\in A$$
49		simp3rl	$$⊢\left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\to z\in A$$
50	49	3ad2ant3	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\in A$$
51	1 2 3 4 5 6 8 15	cdleme1b	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\wedge z\in A\right)\right)\to G\in {\mathrm{Base}}_K$$
52	11 18 13 14 50 51	syl23anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to G\in {\mathrm{Base}}_K$$
53	15 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge T\in A\wedge z\in A\right)\to T\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K$$
54	11 36 50 53	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to T\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K$$
55	15 3	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge T\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\to \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K$$
56	12 54 27 55	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K$$
57	15 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge G\in {\mathrm{Base}}_K\wedge \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K\right)\to G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K$$
58	12 52 56 57	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K$$
59	1 2 3 4 5 6	cdlemeulpq	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\right)\right)\to U\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
60	11 18 13 14 59	syl22anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to U\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
61	15 1 2 3 4	atmod2i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(U\in A\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K\right)\wedge U\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)$$
62	11 48 17 58 60 61	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)$$
63	45 62	eqtr2id	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)=O\underset{\dot{}}{\vee }U$$
64	43	oveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to T\underset{\dot{}}{\vee }V=T\underset{\dot{}}{\vee }U$$
65	41 64	eqtr3d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }Q=T\underset{\dot{}}{\vee }U$$
66	15 2 4	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$$
67	11 36 48 66	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
68	15 4	atbase	$$⊢z\in A\to z\in {\mathrm{Base}}_K$$
69	50 68	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\in {\mathrm{Base}}_K$$
70	15 1 2	latlej1	$$⊢\left(K\in \mathrm{Lat}\wedge T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge z\in {\mathrm{Base}}_K\right)\to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }z\right)$$
71	12 67 69 70	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }z\right)$$
72	2 4	hlatj32	$$⊢\left(K\in \mathrm{HL}\wedge \left(T\in A\wedge U\in A\wedge z\in A\right)\right)\to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }z=\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\vee }U$$
73	11 36 48 50 72	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }z=\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\vee }U$$
74	15 4	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
75	48 74	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to U\in {\mathrm{Base}}_K$$
76	15 2	latj32	$$⊢\left(K\in \mathrm{Lat}\wedge \left(z\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\wedge \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K\right)\right)\to \left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(z\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U$$
77	12 69 75 56 76	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(z\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U$$
78	15 2	latj32	$$⊢\left(K\in \mathrm{Lat}\wedge \left(G\in {\mathrm{Base}}_K\wedge \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\right)\right)\to \left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U=\left(G\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
79	12 52 56 75 78	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U=\left(G\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
80	15 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge z\in A\right)\to P\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K$$
81	11 13 50 80	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K$$
82	1 2 4	hlatlej1	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge z\in A\right)\to P\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }z\right)$$
83	11 13 50 82	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }z\right)$$
84	15 1 2 3 4	atmod3i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge P\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\wedge P\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }z\right)\right)\to P\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\left(P\underset{\dot{}}{\vee }W\right)$$
85	11 13 81 27 83 84	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\left(P\underset{\dot{}}{\vee }W\right)$$
86		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
87	1 2 86 4 5	lhpjat2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to P\underset{\dot{}}{\vee }W=\mathrm{1.}\left(K\right)$$
88	11 18 35 87	syl21anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }W=\mathrm{1.}\left(K\right)$$
89	88	oveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\left(P\underset{\dot{}}{\vee }W\right)=\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)$$
90		hlol	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OL}$$
91	11 90	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to K\in \mathrm{OL}$$
92	15 3 86	olm11	$$⊢\left(K\in \mathrm{OL}\wedge P\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=P\underset{\dot{}}{\vee }z$$
93	91 81 92	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=P\underset{\dot{}}{\vee }z$$
94	85 89 93	3eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=P\underset{\dot{}}{\vee }z$$
95	94	oveq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }Q=\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\vee }Q$$
96	6	oveq2i	$$⊢Q\underset{\dot{}}{\vee }U=Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W\right)$$
97	1 2 4	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
98	11 13 14 97	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
99	15 1 2 3 4	atmod3i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(Q\in A\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\wedge Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }W\right)$$
100	11 14 17 27 98 99	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }W\right)$$
101	96 100	syl5eq	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to Q\underset{\dot{}}{\vee }U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }W\right)$$
102		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
103	1 2 86 4 5	lhpjat2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to Q\underset{\dot{}}{\vee }W=\mathrm{1.}\left(K\right)$$
104	11 18 102 103	syl21anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to Q\underset{\dot{}}{\vee }W=\mathrm{1.}\left(K\right)$$
105	104	oveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }W\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)$$
106	15 3 86	olm11	$$⊢\left(K\in \mathrm{OL}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=P\underset{\dot{}}{\vee }Q$$
107	91 17 106	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=P\underset{\dot{}}{\vee }Q$$
108	101 105 107	3eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to Q\underset{\dot{}}{\vee }U=P\underset{\dot{}}{\vee }Q$$
109	108	oveq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(Q\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
110	15 4	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
111	13 110	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\in {\mathrm{Base}}_K$$
112	15 3	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K$$
113	12 81 27 112	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K$$
114	15 4	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
115	14 114	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to Q\in {\mathrm{Base}}_K$$
116	15 2	latj32	$$⊢\left(K\in \mathrm{Lat}\wedge \left(P\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\right)\right)\to \left(P\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }Q=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
117	12 111 113 115 116	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }Q=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
118	109 117	eqtr4d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(Q\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(P\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }Q$$
119	2 4	hlatj32	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge z\in A\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z=\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\vee }Q$$
120	11 13 14 50 119	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z=\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\vee }Q$$
121	95 118 120	3eqtr4rd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z=\left(Q\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
122	15 2	latj32	$$⊢\left(K\in \mathrm{Lat}\wedge \left(Q\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K\right)\right)\to \left(Q\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U$$
123	12 115 75 113 122	syl13anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(Q\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U$$
124	121 123	eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z=\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U$$
125	124	oveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)$$
126	15 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge z\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K$$
127	12 17 69 126	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K$$
128	15 1 2	latlej2	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge z\in {\mathrm{Base}}_K\right)\to z\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)$$
129	12 17 69 128	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)$$
130	15 1 2 3 4	atmod1i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(z\in A\wedge U\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K\right)\wedge z\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)\right)\to z\underset{\dot{}}{\vee }\left(U\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)\right)=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)$$
131	11 50 75 127 129 130	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\underset{\dot{}}{\vee }\left(U\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)\right)=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)$$
132	8	oveq1i	$$⊢G\underset{\dot{}}{\vee }U=\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }U$$
133	15 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge z\in A\wedge U\in A\right)\to z\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
134	11 50 48 133	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
135	15 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge Q\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K\right)\to Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K$$
136	12 115 113 135	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K$$
137	1 2 4	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge z\in A\wedge U\in A\right)\to U\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }U\right)$$
138	11 50 48 137	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to U\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }U\right)$$
139	15 1 2 3 4	atmod2i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(U\in A\wedge z\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K\right)\wedge U\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }U=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)$$
140	11 48 134 136 138 139	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }U=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)$$
141	132 140	syl5eq	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to G\underset{\dot{}}{\vee }U=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)$$
142	125 131 141	3eqtr4rd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to G\underset{\dot{}}{\vee }U=z\underset{\dot{}}{\vee }\left(U\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)\right)$$
143	15 1 2	latlej1	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge z\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)$$
144	12 17 69 143	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)$$
145	15 1 12 75 17 127 60 144	lattrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)$$
146	15 1 3	latleeqm1	$$⊢\left(K\in \mathrm{Lat}\wedge U\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K\right)\to \left(U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)\leftrightarrow U\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)=U\right)$$
147	12 75 127 146	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)\leftrightarrow U\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)=U\right)$$
148	145 147	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to U\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)=U$$
149	148	oveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\underset{\dot{}}{\vee }\left(U\underset{\dot{}}{\wedge }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }z\right)\right)=z\underset{\dot{}}{\vee }U$$
150	142 149	eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to G\underset{\dot{}}{\vee }U=z\underset{\dot{}}{\vee }U$$
151	150	oveq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(G\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
152	79 151	eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
153	1 2 4	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge T\in A\wedge z\in A\right)\to z\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }z\right)$$
154	11 36 50 153	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }z\right)$$
155	15 1 2 3 4	atmod3i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(z\in A\wedge T\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\wedge z\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }z\right)\right)\to z\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }W\right)$$
156	11 50 54 27 154 155	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }W\right)$$
157		simp33r	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)$$
158	1 2 86 4 5	lhpjat2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\to z\underset{\dot{}}{\vee }W=\mathrm{1.}\left(K\right)$$
159	11 18 157 158	syl21anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to z\underset{\dot{}}{\vee }W=\mathrm{1.}\left(K\right)$$
160	159	oveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }W\right)=\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)$$
161	15 3 86	olm11	$$⊢\left(K\in \mathrm{OL}\wedge T\underset{\dot{}}{\vee }z\in {\mathrm{Base}}_K\right)\to \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=T\underset{\dot{}}{\vee }z$$
162	91 54 161	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=T\underset{\dot{}}{\vee }z$$
163	156 160 162	3eqtrrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to T\underset{\dot{}}{\vee }z=z\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
164	163	oveq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\vee }U=\left(z\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U$$
165	77 152 164	3eqtr4rd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\vee }U=\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U$$
166	73 165	eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }z=\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U$$
167	71 166	breqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)$$
168	65 167	eqbrtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)$$
169	15 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\right)\to \left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
170	12 58 75 169	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
171	15 1 3	latleeqm1	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge \left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)=P\underset{\dot{}}{\vee }Q\right)$$
172	12 17 170 171	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)=P\underset{\dot{}}{\vee }Q\right)$$
173	168 172	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(G\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\vee }U\right)=P\underset{\dot{}}{\vee }Q$$
174	44 63 173	3eqtr2rd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }Q=O\underset{\dot{}}{\vee }V$$
175	34 174	breqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge T\in A\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\wedge \left(S\in A\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\wedge \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\right)\to N\underset{\dot{}}{\le }\left(O\underset{\dot{}}{\vee }V\right)$$