Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  omlfh1N Unicode version

Theorem omlfh1N 29448
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 22197 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
omlfh1.b  |-  B  =  ( Base `  K
)
omlfh1.j  |-  .\/  =  ( join `  K )
omlfh1.m  |-  ./\  =  ( meet `  K )
omlfh1.c  |-  C  =  ( cm `  K
)
Assertion
Ref Expression
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 of Theorem omlfh1N
StepHypRef Expression
1 omllat 29432 . . . . 5  |-  ( K  e.  OML  ->  K  e.  Lat )
2 omlfh1.b . . . . . 6  |-  B  =  ( Base `  K
)
3 eqid 2283 . . . . . 6  |-  ( le
`  K )  =  ( le `  K
)
4 omlfh1.j . . . . . 6  |-  .\/  =  ( join `  K )
5 omlfh1.m . . . . . 6  |-  ./\  =  ( meet `  K )
62, 3, 4, 5latledi 14195 . . . . 5  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  ./\  Y
)  .\/  ( X  ./\ 
Z ) ) ( le `  K ) ( X  ./\  ( Y  .\/  Z ) ) )
71, 6sylan 457 . . . 4  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  ./\  Y
)  .\/  ( X  ./\ 
Z ) ) ( le `  K ) ( X  ./\  ( Y  .\/  Z ) ) )
873adant3 975 . . 3  |-  ( ( 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 ) ) )
91adantr 451 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  Lat )
10 simpr1 961 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  X  e.  B )
11 simpr2 962 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Y  e.  B )
12 simpr3 963 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Z  e.  B )
132, 4latjcl 14156 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  Y  e.  B  /\  Z  e.  B )  ->  ( Y  .\/  Z
)  e.  B )
149, 11, 12, 13syl3anc 1182 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( Y  .\/  Z )  e.  B )
152, 5latmcom 14181 . . . . . . 7  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( Y  .\/  Z )  e.  B )  -> 
( X  ./\  ( Y  .\/  Z ) )  =  ( ( Y 
.\/  Z )  ./\  X ) )
169, 10, 14, 15syl3anc 1182 . . . . . 6  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  ( Y  .\/  Z ) )  =  ( ( Y  .\/  Z
)  ./\  X )
)
17 omlol 29430 . . . . . . . . 9  |-  ( K  e.  OML  ->  K  e.  OL )
1817adantr 451 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  OL )
192, 5latmcl 14157 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  e.  B )
209, 10, 11, 19syl3anc 1182 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  Y )  e.  B )
212, 5latmcl 14157 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Z  e.  B )  ->  ( X  ./\  Z
)  e.  B )
229, 10, 12, 21syl3anc 1182 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  Z )  e.  B )
23 eqid 2283 . . . . . . . . 9  |-  ( oc
`  K )  =  ( oc `  K
)
242, 4, 5, 23oldmj1 29411 . . . . . . . 8  |-  ( ( 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 ) ) ) )
2518, 20, 22, 24syl3anc 1182 . . . . . . 7  |-  ( ( 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 ) ) ) )
262, 4, 5, 23oldmm1 29407 . . . . . . . . 9  |-  ( ( K  e.  OL  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( oc `  K ) `  ( X  ./\  Y ) )  =  ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  Y
) ) )
2718, 10, 11, 26syl3anc 1182 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  ( X  ./\ 
Y ) )  =  ( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  Y )
) )
282, 4, 5, 23oldmm1 29407 . . . . . . . . 9  |-  ( ( K  e.  OL  /\  X  e.  B  /\  Z  e.  B )  ->  ( ( oc `  K ) `  ( X  ./\  Z ) )  =  ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  Z
) ) )
2918, 10, 12, 28syl3anc 1182 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  ( X  ./\ 
Z ) )  =  ( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  Z )
) )
3027, 29oveq12d 5876 . . . . . . 7  |-  ( ( 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
) ) ) )
3125, 30eqtrd 2315 . . . . . 6  |-  ( ( 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
) ) ) )
3216, 31oveq12d 5876 . . . . 5  |-  ( ( 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 ) ) ) ) )
33323adant3 975 . . . 4  |-  ( ( 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 ) ) ) ) )
34 omlop 29431 . . . . . . . . . . 11  |-  ( K  e.  OML  ->  K  e.  OP )
3534adantr 451 . . . . . . . . . 10  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  OP )
362, 23opoccl 29384 . . . . . . . . . 10  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  ( ( oc `  K ) `  X
)  e.  B )
3735, 10, 36syl2anc 642 . . . . . . . . 9  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  X )  e.  B )
382, 23opoccl 29384 . . . . . . . . . 10  |-  ( ( K  e.  OP  /\  Y  e.  B )  ->  ( ( oc `  K ) `  Y
)  e.  B )
3935, 11, 38syl2anc 642 . . . . . . . . 9  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  Y )  e.  B )
402, 4latjcl 14156 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  X
)  e.  B  /\  ( ( oc `  K ) `  Y
)  e.  B )  ->  ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  Y
) )  e.  B
)
419, 37, 39, 40syl3anc 1182 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  Y ) )  e.  B )
422, 23opoccl 29384 . . . . . . . . . 10  |-  ( ( K  e.  OP  /\  Z  e.  B )  ->  ( ( oc `  K ) `  Z
)  e.  B )
4335, 12, 42syl2anc 642 . . . . . . . . 9  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  Z )  e.  B )
442, 4latjcl 14156 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  X
)  e.  B  /\  ( ( oc `  K ) `  Z
)  e.  B )  ->  ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  Z
) )  e.  B
)
459, 37, 43, 44syl3anc 1182 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  Z ) )  e.  B )
462, 5latmcl 14157 . . . . . . . 8  |-  ( ( 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 )
479, 41, 45, 46syl3anc 1182 . . . . . . 7  |-  ( ( 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 )
482, 5latmassOLD 29419 . . . . . . 7  |-  ( ( 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 ) ) ) ) ) )
4918, 14, 10, 47, 48syl13anc 1184 . . . . . 6  |-  ( ( 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 ) ) ) ) ) )
50493adant3 975 . . . . 5  |-  ( ( 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 ) ) ) ) ) )
51 omlfh1.c . . . . . . . . . . . . . 14  |-  C  =  ( cm `  K
)
522, 23, 51cmt2N 29440 . . . . . . . . . . . . 13  |-  ( ( K  e.  OML  /\  X  e.  B  /\  Y  e.  B )  ->  ( X C Y  <-> 
X C ( ( oc `  K ) `
 Y ) ) )
53523adant3r3 1162 . . . . . . . . . . . 12  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X C Y  <->  X C
( ( oc `  K ) `  Y
) ) )
54 simpl 443 . . . . . . . . . . . . 13  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  OML )
552, 4, 5, 23, 51cmtbr3N 29444 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) )
5654, 10, 39, 55syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) )
5753, 56bitrd 244 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
5857biimpa 470 . . . . . . . . . 10  |-  ( ( ( 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 )
) )
5958adantrr 697 . . . . . . . . 9  |-  ( ( ( 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
) ) )
60593impa 1146 . . . . . . . 8  |-  ( ( 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
) ) )
612, 23, 51cmt2N 29440 . . . . . . . . . . . . 13  |-  ( ( K  e.  OML  /\  X  e.  B  /\  Z  e.  B )  ->  ( X C Z  <-> 
X C ( ( oc `  K ) `
 Z ) ) )
62613adant3r2 1161 . . . . . . . . . . . 12  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X C Z  <->  X C
( ( oc `  K ) `  Z
) ) )
632, 4, 5, 23, 51cmtbr3N 29444 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) )
6454, 10, 43, 63syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) )
6562, 64bitrd 244 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
6665biimpa 470 . . . . . . . . . 10  |-  ( ( ( 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 )
) )
6766adantrl 696 . . . . . . . . 9  |-  ( ( ( 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
) ) )
68673impa 1146 . . . . . . . 8  |-  ( ( 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
) ) )
6960, 68oveq12d 5876 . . . . . . 7  |-  ( ( 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 ) ) ) )
702, 5latmmdiN 29424 . . . . . . . . 9  |-  ( ( 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
) ) ) ) )
7118, 10, 41, 45, 70syl13anc 1184 . . . . . . . 8  |-  ( ( 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
) ) ) ) )
72713adant3 975 . . . . . . 7  |-  ( ( 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
) ) ) ) )
732, 5latmmdiN 29424 . . . . . . . . 9  |-  ( ( 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
) ) ) )
7418, 10, 39, 43, 73syl13anc 1184 . . . . . . . 8  |-  ( ( 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 ) ) ) )
75743adant3 975 . . . . . . 7  |-  ( ( 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 ) ) ) )
7669, 72, 753eqtr4d 2325 . . . . . 6  |-  ( ( 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 )
) ) )
7776oveq2d 5874 . . . . 5  |-  ( ( 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 )
) ) ) )
782, 5latmcl 14157 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  Y
)  e.  B  /\  ( ( oc `  K ) `  Z
)  e.  B )  ->  ( ( ( oc `  K ) `
 Y )  ./\  ( ( oc `  K ) `  Z
) )  e.  B
)
799, 39, 43, 78syl3anc 1182 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( ( oc `  K ) `  Y
)  ./\  ( ( oc `  K ) `  Z ) )  e.  B )
802, 5latm12 29420 . . . . . . 7  |-  ( ( 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
) ) ) ) )
8118, 14, 10, 79, 80syl13anc 1184 . . . . . 6  |-  ( ( 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
) ) ) ) )
82813adant3 975 . . . . 5  |-  ( ( 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
) ) ) ) )
8350, 77, 823eqtrd 2319 . . . 4  |-  ( ( 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
) ) ) ) )
842, 4, 5, 23oldmj1 29411 . . . . . . . . . 10  |-  ( ( K  e.  OL  /\  Y  e.  B  /\  Z  e.  B )  ->  ( ( oc `  K ) `  ( Y  .\/  Z ) )  =  ( ( ( oc `  K ) `
 Y )  ./\  ( ( oc `  K ) `  Z
) ) )
8518, 11, 12, 84syl3anc 1182 . . . . . . . . 9  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  ( Y  .\/  Z ) )  =  ( ( ( oc
`  K ) `  Y )  ./\  (
( oc `  K
) `  Z )
) )
8685oveq2d 5874 . . . . . . . 8  |-  ( ( 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 2283 . . . . . . . . . 10  |-  ( 0.
`  K )  =  ( 0. `  K
)
882, 23, 5, 87opnoncon 29398 . . . . . . . . 9  |-  ( ( K  e.  OP  /\  ( Y  .\/  Z )  e.  B )  -> 
( ( Y  .\/  Z )  ./\  ( ( oc `  K ) `  ( Y  .\/  Z ) ) )  =  ( 0. `  K ) )
8935, 14, 88syl2anc 642 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( Y  .\/  Z
)  ./\  ( ( oc `  K ) `  ( Y  .\/  Z ) ) )  =  ( 0. `  K ) )
9086, 89eqtr3d 2317 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( Y  .\/  Z
)  ./\  ( (
( oc `  K
) `  Y )  ./\  ( ( oc `  K ) `  Z
) ) )  =  ( 0. `  K
) )
9190oveq2d 5874 . . . . . 6  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  ( ( Y 
.\/  Z )  ./\  ( ( ( oc
`  K ) `  Y )  ./\  (
( oc `  K
) `  Z )
) ) )  =  ( X  ./\  ( 0. `  K ) ) )
922, 5, 87olm01 29426 . . . . . . 7  |-  ( ( K  e.  OL  /\  X  e.  B )  ->  ( X  ./\  ( 0. `  K ) )  =  ( 0. `  K ) )
9318, 10, 92syl2anc 642 . . . . . 6  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  ( 0. `  K ) )  =  ( 0. `  K
) )
9491, 93eqtrd 2315 . . . . 5  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  ( ( Y 
.\/  Z )  ./\  ( ( ( oc
`  K ) `  Y )  ./\  (
( oc `  K
) `  Z )
) ) )  =  ( 0. `  K
) )
95943adant3 975 . . . 4  |-  ( ( 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 ) )
9633, 83, 953eqtrd 2319 . . 3  |-  ( ( 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 ) )
972, 4latjcl 14156 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( X  ./\  Y )  e.  B  /\  ( X  ./\  Z )  e.  B )  ->  (
( X  ./\  Y
)  .\/  ( X  ./\ 
Z ) )  e.  B )
989, 20, 22, 97syl3anc 1182 . . . . 5  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  ./\  Y
)  .\/  ( X  ./\ 
Z ) )  e.  B )
992, 5latmcl 14157 . . . . . 6  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( Y  .\/  Z )  e.  B )  -> 
( X  ./\  ( Y  .\/  Z ) )  e.  B )
1009, 10, 14, 99syl3anc 1182 . . . . 5  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  ( Y  .\/  Z ) )  e.  B
)
1012, 3, 5, 23, 87omllaw3 29435 . . . . 5  |-  ( ( 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 ) ) ) )
10254, 98, 100, 101syl3anc 1182 . . . 4  |-  ( ( 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 ) ) ) )
1031023adant3 975 . . 3  |-  ( ( 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 ) ) ) )
1048, 96, 103mp2and 660 . 2  |-  ( ( 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 ) ) )
105104eqcomd 2288 1  |-  ( ( 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 ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   class class class wbr 4023   ` cfv 5255  (class class class)co 5858   Basecbs 13148   lecple 13215   occoc 13216   joincjn 14078   meetcmee 14079   0.cp0 14143   Latclat 14151   OPcops 29362   cmccmtN 29363   OLcol 29364   OMLcoml 29365
This theorem is referenced by:  omlfh3N  29449  omlmod1i2N  29450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-undef 6298  df-riota 6304  df-poset 14080  df-lub 14108  df-glb 14109  df-join 14110  df-meet 14111  df-p0 14145  df-lat 14152  df-oposet 29366  df-cmtN 29367  df-ol 29368  df-oml 29369
  Copyright terms: Public domain W3C validator