Theorem dia2dimlem3

Description: Lemma for dia2dim . Define a translation D whose trace is atom V . Part of proof of Lemma M in Crawley p. 121 line 5. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dia2dimlem3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dia2dimlem3.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dia2dimlem3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dia2dimlem3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dia2dimlem3.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dia2dimlem3.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	dia2dimlem3.q	$$⊢Q=\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
	dia2dimlem3.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dia2dimlem3.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
	dia2dimlem3.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
	dia2dimlem3.p	$$⊢\phi \to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
	dia2dimlem3.f	$$⊢\phi \to \left(F\in T\wedge F\left(P\right)\ne P\right)$$
	dia2dimlem3.rf	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }V\right)$$
	dia2dimlem3.uv	$$⊢\phi \to U\ne V$$
	dia2dimlem3.ru	$$⊢\phi \to R\left(F\right)\ne U$$
	dia2dimlem3.rv	$$⊢\phi \to R\left(F\right)\ne V$$
	dia2dimlem3.d	$$⊢\phi \to D\in T$$
	dia2dimlem3.dv	$$⊢\phi \to D\left(Q\right)=F\left(P\right)$$
Assertion	dia2dimlem3	$$⊢\phi \to R\left(D\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dia2dimlem3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dia2dimlem3.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		dia2dimlem3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dia2dimlem3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		dia2dimlem3.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		dia2dimlem3.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
8		dia2dimlem3.q	$$⊢Q=\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
9		dia2dimlem3.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		dia2dimlem3.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
11		dia2dimlem3.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
12		dia2dimlem3.p	$$⊢\phi \to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
13		dia2dimlem3.f	$$⊢\phi \to \left(F\in T\wedge F\left(P\right)\ne P\right)$$
14		dia2dimlem3.rf	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }V\right)$$
15		dia2dimlem3.uv	$$⊢\phi \to U\ne V$$
16		dia2dimlem3.ru	$$⊢\phi \to R\left(F\right)\ne U$$
17		dia2dimlem3.rv	$$⊢\phi \to R\left(F\right)\ne V$$
18		dia2dimlem3.d	$$⊢\phi \to D\in T$$
19		dia2dimlem3.dv	$$⊢\phi \to D\left(Q\right)=F\left(P\right)$$
20	9	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
21	13	simpld	$$⊢\phi \to F\in T$$
22	1 4 5 6	ltrnel	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to \left(F\left(P\right)\in A\wedge \neg F\left(P\right)\underset{\dot{}}{\le }W\right)$$
23	9 21 12 22	syl3anc	$$⊢\phi \to \left(F\left(P\right)\in A\wedge \neg F\left(P\right)\underset{\dot{}}{\le }W\right)$$
24	23	simpld	$$⊢\phi \to F\left(P\right)\in A$$
25	11	simpld	$$⊢\phi \to V\in A$$
26	1 2 4	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge F\left(P\right)\in A\wedge V\in A\right)\to V\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
27	20 24 25 26	syl3anc	$$⊢\phi \to V\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
28	20	hllatd	$$⊢\phi \to K\in \mathrm{Lat}$$
29		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
30	29 4	atbase	$$⊢V\in A\to V\in {\mathrm{Base}}_K$$
31	25 30	syl	$$⊢\phi \to V\in {\mathrm{Base}}_K$$
32	29 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge F\left(P\right)\in A\wedge V\in A\right)\to F\left(P\right)\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K$$
33	20 24 25 32	syl3anc	$$⊢\phi \to F\left(P\right)\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K$$
34	1 4 5 6 7	trlat	$$⊢\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\in T\wedge F\left(P\right)\ne P\right)\right)\to R\left(F\right)\in A$$
35	9 12 13 34	syl3anc	$$⊢\phi \to R\left(F\right)\in A$$
36	10	simpld	$$⊢\phi \to U\in A$$
37	29 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge R\left(F\right)\in A\wedge U\in A\right)\to R\left(F\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
38	20 35 36 37	syl3anc	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
39	29 1 3	latmlem2	$$⊢\left(K\in \mathrm{Lat}\wedge \left(V\in {\mathrm{Base}}_K\wedge F\left(P\right)\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K\wedge R\left(F\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\right)\to \left(V\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\to \left(\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }V\right)\underset{\dot{}}{\le }\left(\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\right)$$
40	28 31 33 38 39	syl13anc	$$⊢\phi \to \left(V\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\to \left(\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }V\right)\underset{\dot{}}{\le }\left(\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\right)$$
41	27 40	mpd	$$⊢\phi \to \left(\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }V\right)\underset{\dot{}}{\le }\left(\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)$$
42	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge U\in A\wedge V\in A\right)\to U\underset{\dot{}}{\vee }V=V\underset{\dot{}}{\vee }U$$
43	20 36 25 42	syl3anc	$$⊢\phi \to U\underset{\dot{}}{\vee }V=V\underset{\dot{}}{\vee }U$$
44	14 43	breqtrd	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\le }\left(V\underset{\dot{}}{\vee }U\right)$$
45	1 2 4	hlatexch2	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\left(F\right)\in A\wedge V\in A\wedge U\in A\right)\wedge R\left(F\right)\ne U\right)\to \left(R\left(F\right)\underset{\dot{}}{\le }\left(V\underset{\dot{}}{\vee }U\right)\to V\underset{\dot{}}{\le }\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\right)$$
46	20 35 25 36 16 45	syl131anc	$$⊢\phi \to \left(R\left(F\right)\underset{\dot{}}{\le }\left(V\underset{\dot{}}{\vee }U\right)\to V\underset{\dot{}}{\le }\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\right)$$
47	44 46	mpd	$$⊢\phi \to V\underset{\dot{}}{\le }\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)$$
48	29 1 3	latleeqm2	$$⊢\left(K\in \mathrm{Lat}\wedge V\in {\mathrm{Base}}_K\wedge R\left(F\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\to \left(V\underset{\dot{}}{\le }\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\leftrightarrow \left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }V=V\right)$$
49	28 31 38 48	syl3anc	$$⊢\phi \to \left(V\underset{\dot{}}{\le }\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\leftrightarrow \left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }V=V\right)$$
50	47 49	mpbid	$$⊢\phi \to \left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }V=V$$
51	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dia2dimlem1	$$⊢\phi \to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
52	1 2 3 4 5 6 7	trlval2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge D\in T\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to R\left(D\right)=\left(Q\underset{\dot{}}{\vee }D\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$
53	9 18 51 52	syl3anc	$$⊢\phi \to R\left(D\right)=\left(Q\underset{\dot{}}{\vee }D\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$
54	8	a1i	$$⊢\phi \to Q=\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
55	54 19	oveq12d	$$⊢\phi \to Q\underset{\dot{}}{\vee }D\left(Q\right)=\left(\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\underset{\dot{}}{\vee }F\left(P\right)$$
56	12	simpld	$$⊢\phi \to P\in A$$
57	29 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge U\in A\right)\to P\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
58	20 56 36 57	syl3anc	$$⊢\phi \to P\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
59	1 2 4	hlatlej1	$$⊢\left(K\in \mathrm{HL}\wedge F\left(P\right)\in A\wedge V\in A\right)\to F\left(P\right)\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
60	20 24 25 59	syl3anc	$$⊢\phi \to F\left(P\right)\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
61	29 1 2 3 4	atmod4i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(F\left(P\right)\in A\wedge P\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge F\left(P\right)\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K\right)\wedge F\left(P\right)\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\underset{\dot{}}{\vee }F\left(P\right)=\left(\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
62	20 24 58 33 60 61	syl131anc	$$⊢\phi \to \left(\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\underset{\dot{}}{\vee }F\left(P\right)=\left(\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
63	2 4	hlatj32	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge U\in A\wedge F\left(P\right)\in A\right)\right)\to \left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }F\left(P\right)=\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U$$
64	20 56 36 24 63	syl13anc	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }F\left(P\right)=\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U$$
65	64	oveq1d	$$⊢\phi \to \left(\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)=\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
66	55 62 65	3eqtrd	$$⊢\phi \to Q\underset{\dot{}}{\vee }D\left(Q\right)=\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
67	66	oveq1d	$$⊢\phi \to \left(Q\underset{\dot{}}{\vee }D\left(Q\right)\right)\underset{\dot{}}{\wedge }W=\left(\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\underset{\dot{}}{\wedge }W$$
68		hlol	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OL}$$
69	20 68	syl	$$⊢\phi \to K\in \mathrm{OL}$$
70	29 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge F\left(P\right)\in A\right)\to P\underset{\dot{}}{\vee }F\left(P\right)\in {\mathrm{Base}}_K$$
71	20 56 24 70	syl3anc	$$⊢\phi \to P\underset{\dot{}}{\vee }F\left(P\right)\in {\mathrm{Base}}_K$$
72	29 4	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
73	36 72	syl	$$⊢\phi \to U\in {\mathrm{Base}}_K$$
74	29 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }F\left(P\right)\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
75	28 71 73 74	syl3anc	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
76	9	simprd	$$⊢\phi \to W\in H$$
77	29 5	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
78	76 77	syl	$$⊢\phi \to W\in {\mathrm{Base}}_K$$
79	29 3	latm32	$$⊢\left(K\in \mathrm{OL}\wedge \left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge F\left(P\right)\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\underset{\dot{}}{\wedge }W=\left(\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
80	69 75 33 78 79	syl13anc	$$⊢\phi \to \left(\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)\right)\underset{\dot{}}{\wedge }W=\left(\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
81	1 2 3 4 5 6 7	trlval2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to R\left(F\right)=\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W$$
82	9 21 12 81	syl3anc	$$⊢\phi \to R\left(F\right)=\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W$$
83	82	oveq1d	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\vee }U=\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }U$$
84	10	simprd	$$⊢\phi \to U\underset{\dot{}}{\le }W$$
85	29 1 2 3 4	atmod4i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(U\in A\wedge P\underset{\dot{}}{\vee }F\left(P\right)\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\wedge U\underset{\dot{}}{\le }W\right)\to \left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }U=\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }W$$
86	20 36 71 78 84 85	syl131anc	$$⊢\phi \to \left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }U=\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }W$$
87	83 86	eqtr2d	$$⊢\phi \to \left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }W=R\left(F\right)\underset{\dot{}}{\vee }U$$
88	87	oveq1d	$$⊢\phi \to \left(\left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)=\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
89	67 80 88	3eqtrd	$$⊢\phi \to \left(Q\underset{\dot{}}{\vee }D\left(Q\right)\right)\underset{\dot{}}{\wedge }W=\left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
90	53 89	eqtr2d	$$⊢\phi \to \left(R\left(F\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)=R\left(D\right)$$
91	41 50 90	3brtr3d	$$⊢\phi \to V\underset{\dot{}}{\le }R\left(D\right)$$
92		hlatl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{AtLat}$$
93	20 92	syl	$$⊢\phi \to K\in \mathrm{AtLat}$$
94		hlop	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OP}$$
95	20 94	syl	$$⊢\phi \to K\in \mathrm{OP}$$
96		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
97		eqid	$$⊢{<}_K={<}_K$$
98	96 97 4	0ltat	$$⊢\left(K\in \mathrm{OP}\wedge V\in A\right)\to \mathrm{0.}\left(K\right){<}_{K}V$$
99	95 25 98	syl2anc	$$⊢\phi \to \mathrm{0.}\left(K\right){<}_{K}V$$
100		hlpos	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Poset}$$
101	20 100	syl	$$⊢\phi \to K\in \mathrm{Poset}$$
102	29 96	op0cl	$$⊢K\in \mathrm{OP}\to \mathrm{0.}\left(K\right)\in {\mathrm{Base}}_K$$
103	95 102	syl	$$⊢\phi \to \mathrm{0.}\left(K\right)\in {\mathrm{Base}}_K$$
104	29 5 6 7	trlcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge D\in T\right)\to R\left(D\right)\in {\mathrm{Base}}_K$$
105	9 18 104	syl2anc	$$⊢\phi \to R\left(D\right)\in {\mathrm{Base}}_K$$
106	29 1 97	pltletr	$$⊢\left(K\in \mathrm{Poset}\wedge \left(\mathrm{0.}\left(K\right)\in {\mathrm{Base}}_K\wedge V\in {\mathrm{Base}}_K\wedge R\left(D\right)\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\mathrm{0.}\left(K\right){<}_{K}V\wedge V\underset{\dot{}}{\le }R\left(D\right)\right)\to \mathrm{0.}\left(K\right){<}_{K}R\left(D\right)\right)$$
107	101 103 31 105 106	syl13anc	$$⊢\phi \to \left(\left(\mathrm{0.}\left(K\right){<}_{K}V\wedge V\underset{\dot{}}{\le }R\left(D\right)\right)\to \mathrm{0.}\left(K\right){<}_{K}R\left(D\right)\right)$$
108	99 91 107	mp2and	$$⊢\phi \to \mathrm{0.}\left(K\right){<}_{K}R\left(D\right)$$
109	29 97 96	opltn0	$$⊢\left(K\in \mathrm{OP}\wedge R\left(D\right)\in {\mathrm{Base}}_K\right)\to \left(\mathrm{0.}\left(K\right){<}_{K}R\left(D\right)\leftrightarrow R\left(D\right)\ne \mathrm{0.}\left(K\right)\right)$$
110	95 105 109	syl2anc	$$⊢\phi \to \left(\mathrm{0.}\left(K\right){<}_{K}R\left(D\right)\leftrightarrow R\left(D\right)\ne \mathrm{0.}\left(K\right)\right)$$
111	108 110	mpbid	$$⊢\phi \to R\left(D\right)\ne \mathrm{0.}\left(K\right)$$
112	111	neneqd	$$⊢\phi \to \neg R\left(D\right)=\mathrm{0.}\left(K\right)$$
113	96 4 5 6 7	trlator0	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge D\in T\right)\to \left(R\left(D\right)\in A\vee R\left(D\right)=\mathrm{0.}\left(K\right)\right)$$
114	9 18 113	syl2anc	$$⊢\phi \to \left(R\left(D\right)\in A\vee R\left(D\right)=\mathrm{0.}\left(K\right)\right)$$
115	114	orcomd	$$⊢\phi \to \left(R\left(D\right)=\mathrm{0.}\left(K\right)\vee R\left(D\right)\in A\right)$$
116	115	ord	$$⊢\phi \to \left(\neg R\left(D\right)=\mathrm{0.}\left(K\right)\to R\left(D\right)\in A\right)$$
117	112 116	mpd	$$⊢\phi \to R\left(D\right)\in A$$
118	1 4	atcmp	$$⊢\left(K\in \mathrm{AtLat}\wedge V\in A\wedge R\left(D\right)\in A\right)\to \left(V\underset{\dot{}}{\le }R\left(D\right)\leftrightarrow V=R\left(D\right)\right)$$
119	93 25 117 118	syl3anc	$$⊢\phi \to \left(V\underset{\dot{}}{\le }R\left(D\right)\leftrightarrow V=R\left(D\right)\right)$$
120	91 119	mpbid	$$⊢\phi \to V=R\left(D\right)$$
121	120	eqcomd	$$⊢\phi \to R\left(D\right)=V$$