# Metamath Proof Explorer

## Theorem cmtcomlemN

Description: Lemma for cmtcomN . ( cmcmlem analog.) (Contributed by NM, 7-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmtcom.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cmtcom.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
Assertion cmtcomlemN ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}{C}{Y}\to {Y}{C}{X}\right)$

### Proof

Step Hyp Ref Expression
1 cmtcom.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cmtcom.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
3 omllat ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{Lat}$
4 3 3ad2ant1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{Lat}$
5 omlop ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OP}$
6 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
7 1 6 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
8 5 7 sylan ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
9 8 3adant3 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
10 simp3 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
11 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
12 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
13 1 11 12 latlej2 ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge {Y}\in {B}\right)\to {Y}{\le }_{{K}}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)$
14 4 9 10 13 syl3anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}{\le }_{{K}}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)$
15 1 12 latjcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\in {B}$
16 4 9 10 15 syl3anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\in {B}$
17 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
18 1 11 17 latleeqm2 ${⊢}\left({K}\in \mathrm{Lat}\wedge {Y}\in {B}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\in {B}\right)\to \left({Y}{\le }_{{K}}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)↔\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}={Y}\right)$
19 4 10 16 18 syl3anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({Y}{\le }_{{K}}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)↔\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}={Y}\right)$
20 14 19 mpbid ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}={Y}$
21 20 oveq2d ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}\right)=\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right){Y}$
22 omlol ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OL}$
23 22 3ad2ant1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OL}$
24 5 3ad2ant1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OP}$
25 1 6 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
26 24 10 25 syl2anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
27 1 12 latjcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
28 4 9 26 27 syl3anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
29 1 17 latmassOLD ${⊢}\left({K}\in \mathrm{OL}\wedge \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)\mathrm{meet}\left({K}\right){Y}=\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}\right)$
30 23 28 16 10 29 syl13anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)\mathrm{meet}\left({K}\right){Y}=\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}\right)$
31 1 12 17 6 oldmm1 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)=\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)$
32 22 31 syl3an1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)=\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)$
33 32 oveq1d ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}=\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right){Y}$
34 21 30 33 3eqtr4rd ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}=\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)\mathrm{meet}\left({K}\right){Y}$
35 34 adantr ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}=\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)\mathrm{meet}\left({K}\right){Y}$
36 1 12 17 6 oldmj4 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)={X}\mathrm{meet}\left({K}\right){Y}$
37 22 36 syl3an1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)={X}\mathrm{meet}\left({K}\right){Y}$
38 1 12 17 6 oldmj2 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)={X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)$
39 22 38 syl3an1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)={X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)$
40 37 39 oveq12d ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)$
41 40 eqeq2d ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}=\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)↔{X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)$
42 41 biimpar ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to {X}=\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)$
43 42 fveq2d ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)=\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)$
44 1 12 17 6 oldmj4 ${⊢}\left({K}\in \mathrm{OL}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)$
45 23 28 16 44 syl3anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)$
46 45 adantr ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)$
47 43 46 eqtr2d ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)=\mathrm{oc}\left({K}\right)\left({X}\right)$
48 47 oveq1d ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\right)\mathrm{meet}\left({K}\right){Y}=\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right){Y}$
49 35 48 eqtrd ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}=\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right){Y}$
50 49 oveq2d ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}\right)=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right){Y}\right)$
51 simp1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OML}$
52 1 17 latmcl ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\mathrm{meet}\left({K}\right){Y}\in {B}$
53 3 52 syl3an1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\mathrm{meet}\left({K}\right){Y}\in {B}$
54 51 53 10 3jca ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({K}\in \mathrm{OML}\wedge {X}\mathrm{meet}\left({K}\right){Y}\in {B}\wedge {Y}\in {B}\right)$
55 1 11 17 latmle2 ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}\mathrm{meet}\left({K}\right){Y}\right){\le }_{{K}}{Y}$
56 3 55 syl3an1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}\mathrm{meet}\left({K}\right){Y}\right){\le }_{{K}}{Y}$
57 1 11 12 17 6 omllaw2N ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\mathrm{meet}\left({K}\right){Y}\in {B}\wedge {Y}\in {B}\right)\to \left(\left({X}\mathrm{meet}\left({K}\right){Y}\right){\le }_{{K}}{Y}\to \left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}\right)={Y}\right)$
58 54 56 57 sylc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}\right)={Y}$
59 58 adantr ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{meet}\left({K}\right){Y}\right)={Y}$
60 1 17 latmcom ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\mathrm{meet}\left({K}\right){Y}={Y}\mathrm{meet}\left({K}\right){X}$
61 3 60 syl3an1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\mathrm{meet}\left({K}\right){Y}={Y}\mathrm{meet}\left({K}\right){X}$
62 1 17 latmcom ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right){Y}={Y}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({X}\right)$
63 4 9 10 62 syl3anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right){Y}={Y}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({X}\right)$
64 61 63 oveq12d ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right){Y}\right)=\left({Y}\mathrm{meet}\left({K}\right){X}\right)\mathrm{join}\left({K}\right)\left({Y}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({X}\right)\right)$
65 64 adantr ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to \left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right){Y}\right)=\left({Y}\mathrm{meet}\left({K}\right){X}\right)\mathrm{join}\left({K}\right)\left({Y}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({X}\right)\right)$
66 50 59 65 3eqtr3d ${⊢}\left(\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)\to {Y}=\left({Y}\mathrm{meet}\left({K}\right){X}\right)\mathrm{join}\left({K}\right)\left({Y}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({X}\right)\right)$
67 66 ex ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\to {Y}=\left({Y}\mathrm{meet}\left({K}\right){X}\right)\mathrm{join}\left({K}\right)\left({Y}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({X}\right)\right)\right)$
68 1 12 17 6 2 cmtvalN ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}{C}{Y}↔{X}=\left({X}\mathrm{meet}\left({K}\right){Y}\right)\mathrm{join}\left({K}\right)\left({X}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)$
69 1 12 17 6 2 cmtvalN ${⊢}\left({K}\in \mathrm{OML}\wedge {Y}\in {B}\wedge {X}\in {B}\right)\to \left({Y}{C}{X}↔{Y}=\left({Y}\mathrm{meet}\left({K}\right){X}\right)\mathrm{join}\left({K}\right)\left({Y}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({X}\right)\right)\right)$
70 69 3com23 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({Y}{C}{X}↔{Y}=\left({Y}\mathrm{meet}\left({K}\right){X}\right)\mathrm{join}\left({K}\right)\left({Y}\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({X}\right)\right)\right)$
71 67 68 70 3imtr4d ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}{C}{Y}\to {Y}{C}{X}\right)$