Metamath Proof Explorer

Theorem omlfh1N

Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in Kalmbach p. 25. ( fh1 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses omlfh1.b 
|- B = ( Base ` K )
omlfh1.j 
|- .\/ = ( join ` K )
omlfh1.m 
|- ./\ = ( meet ` K )
omlfh1.c 
|- C = ( cm ` K )
Assertion omlfh1N 
|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) )

Proof

Step Hyp Ref Expression
1 omlfh1.b 
 |-  B = ( Base ` K )
2 omlfh1.j 
 |-  .\/ = ( join ` K )
3 omlfh1.m 
 |-  ./\ = ( meet ` K )
4 omlfh1.c 
 |-  C = ( cm ` K )
5 omllat 
 |-  ( K e. OML -> K e. Lat )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 1 6 2 3 latledi 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) )
8 5 7 sylan 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) )
9 8 3adant3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) )
10 5 adantr 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
11 simpr1 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
12 simpr2 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
13 simpr3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
14 1 2 latjcl 
 |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y .\/ Z ) e. B )
15 10 12 13 14 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .\/ Z ) e. B )
16 1 3 latmcom 
 |-  ( ( K e. Lat /\ X e. B /\ ( Y .\/ Z ) e. B ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( Y .\/ Z ) ./\ X ) )
17 10 11 15 16 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( Y .\/ Z ) ./\ X ) )
18 omlol 
 |-  ( K e. OML -> K e. OL )
19 18 adantr 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OL )
20 1 3 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
21 10 11 12 20 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Y ) e. B )
22 1 3 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Z e. B ) -> ( X ./\ Z ) e. B )
23 10 11 13 22 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Z ) e. B )
24 eqid 
 |-  ( oc ` K ) = ( oc ` K )
25 1 2 3 24 oldmj1 
 |-  ( ( K e. OL /\ ( X ./\ Y ) e. B /\ ( X ./\ Z ) e. B ) -> ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) = ( ( ( oc ` K ) ` ( X ./\ Y ) ) ./\ ( ( oc ` K ) ` ( X ./\ Z ) ) ) )
26 19 21 23 25 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) = ( ( ( oc ` K ) ` ( X ./\ Y ) ) ./\ ( ( oc ` K ) ` ( X ./\ Z ) ) ) )
27 1 2 3 24 oldmm1 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` ( X ./\ Y ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) )
28 19 11 12 27 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( X ./\ Y ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) )
29 1 2 3 24 oldmm1 
 |-  ( ( K e. OL /\ X e. B /\ Z e. B ) -> ( ( oc ` K ) ` ( X ./\ Z ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) )
30 19 11 13 29 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( X ./\ Z ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) )
31 28 30 oveq12d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` ( X ./\ Y ) ) ./\ ( ( oc ` K ) ` ( X ./\ Z ) ) ) = ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) )
32 26 31 eqtrd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) = ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) )
33 17 32 oveq12d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
34 33 3adant3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
35 omlop 
 |-  ( K e. OML -> K e. OP )
36 35 adantr 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OP )
37 1 24 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
38 36 11 37 syl2anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` X ) e. B )
39 1 24 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
40 36 12 39 syl2anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` Y ) e. B )
41 1 2 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) e. B )
42 10 38 40 41 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) e. B )
43 1 24 opoccl 
 |-  ( ( K e. OP /\ Z e. B ) -> ( ( oc ` K ) ` Z ) e. B )
44 36 13 43 syl2anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` Z ) e. B )
45 1 2 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) e. B )
46 10 38 44 45 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) e. B )
47 1 3 latmcl 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) e. B /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) e. B ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) e. B )
48 10 42 46 47 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) e. B )
49 1 3 latmassOLD 
 |-  ( ( K e. OL /\ ( ( Y .\/ Z ) e. B /\ X e. B /\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) e. B ) ) -> ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) ) )
50 19 15 11 48 49 syl13anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) ) )
51 50 3adant3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) ) )
52 1 24 4 cmt2N 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X C ( ( oc ` K ) ` Y ) ) )
53 52 3adant3r3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Y <-> X C ( ( oc ` K ) ` Y ) ) )
54 simpl 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OML )
55 1 2 3 24 4 cmtbr3N 
 |-  ( ( K e. OML /\ X e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( X C ( ( oc ` K ) ` Y ) <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) ) )
56 54 11 40 55 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C ( ( oc ` K ) ` Y ) <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) ) )
57 53 56 bitrd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Y <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) ) )
58 57 biimpa 
 |-  ( ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) )
59 58 adantrr 
 |-  ( ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) )
60 59 3impa 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) )
61 1 24 4 cmt2N 
 |-  ( ( K e. OML /\ X e. B /\ Z e. B ) -> ( X C Z <-> X C ( ( oc ` K ) ` Z ) ) )
62 61 3adant3r2 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Z <-> X C ( ( oc ` K ) ` Z ) ) )
63 1 2 3 24 4 cmtbr3N 
 |-  ( ( K e. OML /\ X e. B /\ ( ( oc ` K ) ` Z ) e. B ) -> ( X C ( ( oc ` K ) ` Z ) <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
64 54 11 44 63 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C ( ( oc ` K ) ` Z ) <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
65 62 64 bitrd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Z <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
66 65 biimpa 
 |-  ( ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Z ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) )
67 66 adantrl 
 |-  ( ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) )
68 67 3impa 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) )
69 60 68 oveq12d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) ./\ ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( X ./\ ( ( oc ` K ) ` Y ) ) ./\ ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
70 1 3 latmmdiN 
 |-  ( ( K e. OL /\ ( X e. B /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) e. B /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) e. B ) ) -> ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) ./\ ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
71 19 11 42 46 70 syl13anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) ./\ ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
72 71 3adant3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) ./\ ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
73 1 3 latmmdiN 
 |-  ( ( K e. OL /\ ( X e. B /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) ) -> ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) = ( ( X ./\ ( ( oc ` K ) ` Y ) ) ./\ ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
74 19 11 40 44 73 syl13anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) = ( ( X ./\ ( ( oc ` K ) ` Y ) ) ./\ ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
75 74 3adant3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) = ( ( X ./\ ( ( oc ` K ) ` Y ) ) ./\ ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
76 69 72 75 3eqtr4d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) )
77 76 oveq2d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) ) = ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
78 1 3 latmcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) -> ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) e. B )
79 10 40 44 78 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) e. B )
80 1 3 latm12 
 |-  ( ( K e. OL /\ ( ( Y .\/ Z ) e. B /\ X e. B /\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) e. B ) ) -> ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
81 19 15 11 79 80 syl13anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
82 81 3adant3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
83 51 77 82 3eqtrd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
84 1 2 3 24 oldmj1 
 |-  ( ( K e. OL /\ Y e. B /\ Z e. B ) -> ( ( oc ` K ) ` ( Y .\/ Z ) ) = ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) )
85 19 12 13 84 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( Y .\/ Z ) ) = ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) )
86 85 oveq2d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) ./\ ( ( oc ` K ) ` ( Y .\/ Z ) ) ) = ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) )
87 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
88 1 24 3 87 opnoncon 
 |-  ( ( K e. OP /\ ( Y .\/ Z ) e. B ) -> ( ( Y .\/ Z ) ./\ ( ( oc ` K ) ` ( Y .\/ Z ) ) ) = ( 0. ` K ) )
89 36 15 88 syl2anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) ./\ ( ( oc ` K ) ` ( Y .\/ Z ) ) ) = ( 0. ` K ) )
90 86 89 eqtr3d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) = ( 0. ` K ) )
91 90 oveq2d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( 0. ` K ) ) )
92 1 3 87 olm01 
 |-  ( ( K e. OL /\ X e. B ) -> ( X ./\ ( 0. ` K ) ) = ( 0. ` K ) )
93 19 11 92 syl2anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( 0. ` K ) ) = ( 0. ` K ) )
94 91 93 eqtrd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( 0. ` K ) )
95 94 3adant3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( 0. ` K ) )
96 34 83 95 3eqtrd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( 0. ` K ) )
97 1 2 latjcl 
 |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ ( X ./\ Z ) e. B ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) e. B )
98 10 21 23 97 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) e. B )
99 1 3 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( Y .\/ Z ) e. B ) -> ( X ./\ ( Y .\/ Z ) ) e. B )
100 10 11 15 99 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( Y .\/ Z ) ) e. B )
101 1 6 3 24 87 omllaw3 
 |-  ( ( K e. OML /\ ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) e. B /\ ( X ./\ ( Y .\/ Z ) ) e. B ) -> ( ( ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) /\ ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( 0. ` K ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) = ( X ./\ ( Y .\/ Z ) ) ) )
102 54 98 100 101 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) /\ ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( 0. ` K ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) = ( X ./\ ( Y .\/ Z ) ) ) )
103 102 3adant3 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) /\ ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( 0. ` K ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) = ( X ./\ ( Y .\/ Z ) ) ) )
104 9 96 103 mp2and 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) = ( X ./\ ( Y .\/ Z ) ) )
105 104 eqcomd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) )