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 = ( Base ` K )
cmtcom.c 
|- C = ( cm ` K )
Assertion cmtcomlemN 
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y -> Y C X ) )

Proof

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