Theorem cdlemg19a

Description: Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013)

	Ref	Expression
Hypotheses	cdlemg12.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemg12.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemg12.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdlemg12.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemg12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemg12.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemg12b.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
Assertion	cdlemg19a	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)=\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W$$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdlemg12.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdlemg12.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdlemg12.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdlemg12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdlemg12.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		cdlemg12b.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
8		simp11l	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to K\in \mathrm{HL}$$
9	8	hllatd	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to K\in \mathrm{Lat}$$
10		simp12l	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to P\in A$$
11		simp11	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		simp21	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(F\in T\wedge G\in T\right)$$
13	1 4 5 6	ltrncoat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in T\wedge G\in T\right)\wedge P\in A\right)\to F\left(G\left(P\right)\right)\in A$$
14	11 12 10 13	syl3anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to F\left(G\left(P\right)\right)\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 F\left(G\left(P\right)\right)\in A\right)\to P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\in {\mathrm{Base}}_K$$
17	8 10 14 16	syl3anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\in {\mathrm{Base}}_K$$
18		simp13l	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to Q\in A$$
19	1 4 5 6	ltrncoat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in T\wedge G\in T\right)\wedge Q\in A\right)\to F\left(G\left(Q\right)\right)\in A$$
20	11 12 18 19	syl3anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to F\left(G\left(Q\right)\right)\in A$$
21	15 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge F\left(G\left(Q\right)\right)\in A\right)\to Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\in {\mathrm{Base}}_K$$
22	8 18 20 21	syl3anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\in {\mathrm{Base}}_K$$
23	15 1 3	latmle1	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\in {\mathrm{Base}}_K\right)\to \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)$$
24	9 17 22 23	syl3anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)$$
25	1 2 3 4 5 6 7	cdlemg18	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }W$$
26	1 2 3 4 5 6 7	cdlemg18d	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\in A$$
27	15 4	atbase	$$⊢\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\in A\to \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\in {\mathrm{Base}}_K$$
28	26 27	syl	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\in {\mathrm{Base}}_K$$
29		simp11r	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to W\in H$$
30	15 5	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
31	29 30	syl	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to W\in {\mathrm{Base}}_K$$
32	15 1 3	latlem12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
33	9 28 17 31 32	syl13anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
34	24 25 33	mpbi2and	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\right)$$
35		hlatl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{AtLat}$$
36	8 35	syl	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to K\in \mathrm{AtLat}$$
37		simp12	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
38		simp13	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
39		simp21l	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to F\in T$$
40		simp21r	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to G\in T$$
41		simp32	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q$$
42	1 2 3 4 5 6	cdlemg11a	$$⊢\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 \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(F\in T\wedge G\in T\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\right)\right)\to F\left(G\left(P\right)\right)\ne P$$
43	11 37 38 39 40 41 42	syl123anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to F\left(G\left(P\right)\right)\ne P$$
44	43	necomd	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to P\ne F\left(G\left(P\right)\right)$$
45	1 2 3 4 5	lhpat	$$⊢\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(F\left(G\left(P\right)\right)\in A\wedge P\ne F\left(G\left(P\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\in A$$
46	11 37 14 44 45	syl112anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\in A$$
47	1 4	atcmp	$$⊢\left(K\in \mathrm{AtLat}\wedge \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\in A\wedge \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\in A\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)=\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\right)$$
48	36 26 46 47	syl3anc	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)=\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W\right)$$
49	34 48	mpbid	$$⊢\left(\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 \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(F\in T\wedge G\in T\right)\wedge P\ne Q\wedge G\left(P\right)\ne P\right)\wedge \left(R\left(G\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge F\left(G\left(P\right)\right)\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\ne P\underset{\dot{}}{\vee }Q\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }F\left(G\left(Q\right)\right)\right)=\left(P\underset{\dot{}}{\vee }F\left(G\left(P\right)\right)\right)\underset{\dot{}}{\wedge }W$$