Theorem dia2dimlem2

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

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

Proof

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