# Metamath Proof Explorer

## Theorem doca2N

Description: Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses doca2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
doca2.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
doca2.n
Assertion doca2N

### Proof

Step Hyp Ref Expression
1 doca2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 doca2.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
3 doca2.n
4 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
5 4 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {K}\in \mathrm{OL}$
6 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
7 6 1 2 diadmclN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {X}\in {\mathrm{Base}}_{{K}}$
8 6 1 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
9 8 ad2antlr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {W}\in {\mathrm{Base}}_{{K}}$
10 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
11 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
12 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
13 6 10 11 12 oldmm1 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\in {\mathrm{Base}}_{{K}}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){W}\right)=\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
14 5 7 9 13 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){W}\right)=\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
15 14 oveq1d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{meet}\left({K}\right){W}=\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}$
16 15 eqcomd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}=\mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{meet}\left({K}\right){W}$
17 16 fveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right)=\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{meet}\left({K}\right){W}\right)$
18 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
19 18 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {K}\in \mathrm{Lat}$
20 6 11 latmcl ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {\mathrm{Base}}_{{K}}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\to {X}\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}$
21 19 7 9 20 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {X}\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}$
22 6 10 11 12 oldmm2 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{meet}\left({K}\right){W}\right)=\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
23 5 21 9 22 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{meet}\left({K}\right){W}\right)=\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
24 17 23 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right)=\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
25 24 oveq1d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)=\left(\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
26 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
27 26 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {K}\in \mathrm{OP}$
28 6 12 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}$
29 27 9 28 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}$
30 6 10 latjass ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}\wedge \mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}\right)\right)\to \left(\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)=\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)$
31 19 21 29 29 30 syl13anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)=\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)$
32 6 10 latjidm ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)=\mathrm{oc}\left({K}\right)\left({W}\right)$
33 19 29 32 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)=\mathrm{oc}\left({K}\right)\left({W}\right)$
34 33 oveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
35 31 34 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)=\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
36 25 35 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)=\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)$
37 36 oveq1d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\mathrm{oc}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}=\left(\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}$
38 hloml ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OML}$
39 38 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {K}\in \mathrm{OML}$
40 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
41 6 40 11 latmle2 ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {\mathrm{Base}}_{{K}}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\to \left({X}\mathrm{meet}\left({K}\right){W}\right){\le }_{{K}}{W}$
42 19 7 9 41 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left({X}\mathrm{meet}\left({K}\right){W}\right){\le }_{{K}}{W}$
43 6 40 10 11 12 omlspjN ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\wedge \left({X}\mathrm{meet}\left({K}\right){W}\right){\le }_{{K}}{W}\right)\to \left(\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}={X}\mathrm{meet}\left({K}\right){W}$
44 39 21 9 42 43 syl121anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\left({X}\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}={X}\mathrm{meet}\left({K}\right){W}$
45 40 1 2 diadmleN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {X}{\le }_{{K}}{W}$
46 6 40 11 latleeqm1 ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {\mathrm{Base}}_{{K}}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\to \left({X}{\le }_{{K}}{W}↔{X}\mathrm{meet}\left({K}\right){W}={X}\right)$
47 19 7 9 46 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left({X}{\le }_{{K}}{W}↔{X}\mathrm{meet}\left({K}\right){W}={X}\right)$
48 45 47 mpbid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {X}\mathrm{meet}\left({K}\right){W}={X}$
49 37 44 48 3eqtrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {X}=\left(\mathrm{oc}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}$
50 49 fveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to {I}\left({X}\right)={I}\left(\left(\mathrm{oc}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right)$
51 6 12 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {\mathrm{Base}}_{{K}}$
52 27 7 51 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {\mathrm{Base}}_{{K}}$
53 6 10 latjcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}$
54 19 52 29 53 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}$
55 6 11 latmcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}$
56 19 54 9 55 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}$
57 6 40 11 latmle2 ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\in {\mathrm{Base}}_{{K}}\wedge {W}\in {\mathrm{Base}}_{{K}}\right)\to \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right){\le }_{{K}}{W}$
58 19 54 9 57 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right){\le }_{{K}}{W}$
59 6 40 1 2 diaeldm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\in \mathrm{dom}{I}↔\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}\wedge \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right){\le }_{{K}}{W}\right)\right)$
60 59 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\in \mathrm{dom}{I}↔\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\in {\mathrm{Base}}_{{K}}\wedge \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\right){\le }_{{K}}{W}\right)\right)$
61 56 58 60 mpbir2and ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{dom}{I}\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{meet}\left({K}\right){W}\in \mathrm{dom}{I}$
62 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
63 10 11 12 1 62 2 3 diaocN
64 61 63 syldan
65 10 11 12 1 62 2 3 diaocN
66 65 fveq2d
67 50 64 66 3eqtrrd