# 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) ) ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) ) ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) ) ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`