Metamath Proof Explorer

Theorem cmtbr3N

Description: Alternate definition for the commutes relation. Lemma 3 of Kalmbach p. 23. ( cmbr3 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmtbr2.b 
|- B = ( Base ` K )
cmtbr2.j 
|- .\/ = ( join ` K )
cmtbr2.m 
|- ./\ = ( meet ` K )
cmtbr2.o 
|- ._|_ = ( oc ` K )
cmtbr2.c 
|- C = ( cm ` K )
Assertion cmtbr3N 
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )

Proof

Step Hyp Ref Expression
1 cmtbr2.b 
 |-  B = ( Base ` K )
2 cmtbr2.j 
 |-  .\/ = ( join ` K )
3 cmtbr2.m 
 |-  ./\ = ( meet ` K )
4 cmtbr2.o 
 |-  ._|_ = ( oc ` K )
5 cmtbr2.c 
 |-  C = ( cm ` K )
6 1 5 cmtcomN 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> Y C X ) )
7 1 2 3 4 5 cmtbr2N 
 |-  ( ( K e. OML /\ Y e. B /\ X e. B ) -> ( Y C X <-> Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )
8 7 3com23 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y C X <-> Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )
9 6 8 bitrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )
10 oveq2 
 |-  ( Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) -> ( X ./\ Y ) = ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )
11 10 adantl 
 |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) -> ( X ./\ Y ) = ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )
12 omlol 
 |-  ( K e. OML -> K e. OL )
13 12 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OL )
14 simp2 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )
15 omllat 
 |-  ( K e. OML -> K e. Lat )
16 15 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )
17 simp3 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )
18 1 2 latjcl 
 |-  ( ( K e. Lat /\ Y e. B /\ X e. B ) -> ( Y .\/ X ) e. B )
19 16 17 14 18 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .\/ X ) e. B )
20 omlop 
 |-  ( K e. OML -> K e. OP )
21 20 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP )
22 1 4 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
23 21 14 22 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
24 1 2 latjcl 
 |-  ( ( K e. Lat /\ Y e. B /\ ( ._|_ ` X ) e. B ) -> ( Y .\/ ( ._|_ ` X ) ) e. B )
25 16 17 23 24 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .\/ ( ._|_ ` X ) ) e. B )
26 1 3 latmassOLD 
 |-  ( ( K e. OL /\ ( X e. B /\ ( Y .\/ X ) e. B /\ ( Y .\/ ( ._|_ ` X ) ) e. B ) ) -> ( ( X ./\ ( Y .\/ X ) ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) = ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )
27 13 14 19 25 26 syl13anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( Y .\/ X ) ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) = ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )
28 1 2 latjcom 
 |-  ( ( K e. Lat /\ Y e. B /\ X e. B ) -> ( Y .\/ X ) = ( X .\/ Y ) )
29 16 17 14 28 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .\/ X ) = ( X .\/ Y ) )
30 29 oveq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( Y .\/ X ) ) = ( X ./\ ( X .\/ Y ) ) )
31 1 2 3 latabs2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ ( X .\/ Y ) ) = X )
32 15 31 syl3an1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( X .\/ Y ) ) = X )
33 30 32 eqtrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( Y .\/ X ) ) = X )
34 1 2 latjcom 
 |-  ( ( K e. Lat /\ Y e. B /\ ( ._|_ ` X ) e. B ) -> ( Y .\/ ( ._|_ ` X ) ) = ( ( ._|_ ` X ) .\/ Y ) )
35 16 17 23 34 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .\/ ( ._|_ ` X ) ) = ( ( ._|_ ` X ) .\/ Y ) )
36 33 35 oveq12d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( Y .\/ X ) ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) = ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )
37 27 36 eqtr3d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) = ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )
38 37 adantr 
 |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) -> ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) = ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )
39 11 38 eqtr2d 
 |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) )
40 39 ex 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )
41 9 40 sylbid 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )
42 simp1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OML )
43 1 4 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
44 21 17 43 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
45 1 3 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X ./\ ( ._|_ ` Y ) ) e. B )
46 16 14 44 45 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ._|_ ` Y ) ) e. B )
47 42 46 14 3jca 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( K e. OML /\ ( X ./\ ( ._|_ ` Y ) ) e. B /\ X e. B ) )
48 eqid 
 |-  ( le ` K ) = ( le ` K )
49 1 48 3 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X ./\ ( ._|_ ` Y ) ) ( le ` K ) X )
50 16 14 44 49 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ._|_ ` Y ) ) ( le ` K ) X )
51 1 48 2 3 4 omllaw2N 
 |-  ( ( K e. OML /\ ( X ./\ ( ._|_ ` Y ) ) e. B /\ X e. B ) -> ( ( X ./\ ( ._|_ ` Y ) ) ( le ` K ) X -> ( ( X ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) ) = X ) )
52 47 50 51 sylc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) ) = X )
53 1 4 opoccl 
 |-  ( ( K e. OP /\ ( X ./\ ( ._|_ ` Y ) ) e. B ) -> ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) e. B )
54 21 46 53 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) e. B )
55 1 3 latmcl 
 |-  ( ( K e. Lat /\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) e. B /\ X e. B ) -> ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) e. B )
56 16 54 14 55 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) e. B )
57 1 2 latjcom 
 |-  ( ( K e. Lat /\ ( X ./\ ( ._|_ ` Y ) ) e. B /\ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) e. B ) -> ( ( X ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) ) = ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )
58 16 46 56 57 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) ) = ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )
59 52 58 eqtr3d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X = ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )
60 59 adantr 
 |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) -> X = ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )
61 1 2 3 4 oldmm3N 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) = ( ( ._|_ ` X ) .\/ Y ) )
62 12 61 syl3an1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) = ( ( ._|_ ` X ) .\/ Y ) )
63 62 oveq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ) = ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )
64 1 3 latmcom 
 |-  ( ( K e. Lat /\ X e. B /\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) e. B ) -> ( X ./\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) )
65 16 14 54 64 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) )
66 63 65 eqtr3d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) )
67 66 eqeq1d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) <-> ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) = ( X ./\ Y ) ) )
68 oveq1 
 |-  ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) = ( X ./\ Y ) -> ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )
69 67 68 syl6bi 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) -> ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )
70 69 imp 
 |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) -> ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )
71 60 70 eqtrd 
 |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) -> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )
72 71 ex 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) -> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )
73 1 2 3 4 5 cmtvalN 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )
74 72 73 sylibrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) -> X C Y ) )
75 41 74 impbid 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )