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

Theorem omlfh1N 28352
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 22045 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 28336 . . . . 5  |-  ( K  e.  OML  ->  K  e.  Lat )
2 omlfh1.b . . . . . 6  |-  B  =  ( Base `  K
)
3 eqid 2253 . . . . . 6  |-  ( le
`  K )  =  ( le `  K
)
4 omlfh1.j . . . . . 6  |-  .\/  =  ( join `  K )
5 omlfh1.m . . . . . 6  |-  ./\  =  ( meet `  K )
62, 3, 4, 5latledi 14039 . . . . 5  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  ./\  Y
)  .\/  ( X  ./\ 
Z ) ) ( le `  K ) ( X  ./\  ( Y  .\/  Z ) ) )
71, 6sylan 459 . . . 4  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  ./\  Y
)  .\/  ( X  ./\ 
Z ) ) ( le `  K ) ( X  ./\  ( Y  .\/  Z ) ) )
873adant3 980 . . 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 453 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  Lat )
10 simpr1 966 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  X  e.  B )
11 simpr2 967 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Y  e.  B )
12 simpr3 968 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Z  e.  B )
132, 4latjcl 14000 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  Y  e.  B  /\  Z  e.  B )  ->  ( Y  .\/  Z
)  e.  B )
149, 11, 12, 13syl3anc 1187 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( Y  .\/  Z )  e.  B )
152, 5latmcom 14025 . . . . . . 7  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( Y  .\/  Z )  e.  B )  -> 
( X  ./\  ( Y  .\/  Z ) )  =  ( ( Y 
.\/  Z )  ./\  X ) )
169, 10, 14, 15syl3anc 1187 . . . . . 6  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  ( Y  .\/  Z ) )  =  ( ( Y  .\/  Z
)  ./\  X )
)
17 omlol 28334 . . . . . . . . 9  |-  ( K  e.  OML  ->  K  e.  OL )
1817adantr 453 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  OL )
192, 5latmcl 14001 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  e.  B )
209, 10, 11, 19syl3anc 1187 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  Y )  e.  B )
212, 5latmcl 14001 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Z  e.  B )  ->  ( X  ./\  Z
)  e.  B )
229, 10, 12, 21syl3anc 1187 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  Z )  e.  B )
23 eqid 2253 . . . . . . . . 9  |-  ( oc
`  K )  =  ( oc `  K
)
242, 4, 5, 23oldmj1 28315 . . . . . . . 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 1187 . . . . . . 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 28311 . . . . . . . . 9  |-  ( ( K  e.  OL  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( oc `  K ) `  ( X  ./\  Y ) )  =  ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  Y
) ) )
2718, 10, 11, 26syl3anc 1187 . . . . . . . 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 28311 . . . . . . . . 9  |-  ( ( K  e.  OL  /\  X  e.  B  /\  Z  e.  B )  ->  ( ( oc `  K ) `  ( X  ./\  Z ) )  =  ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  Z
) ) )
2918, 10, 12, 28syl3anc 1187 . . . . . . . 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 5728 . . . . . . 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 2285 . . . . . 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 5728 . . . . 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 980 . . . 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 28335 . . . . . . . . . . 11  |-  ( K  e.  OML  ->  K  e.  OP )
3534adantr 453 . . . . . . . . . 10  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  OP )
362, 23opoccl 28288 . . . . . . . . . 10  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  ( ( oc `  K ) `  X
)  e.  B )
3735, 10, 36syl2anc 645 . . . . . . . . 9  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  X )  e.  B )
382, 23opoccl 28288 . . . . . . . . . 10  |-  ( ( K  e.  OP  /\  Y  e.  B )  ->  ( ( oc `  K ) `  Y
)  e.  B )
3935, 11, 38syl2anc 645 . . . . . . . . 9  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  Y )  e.  B )
402, 4latjcl 14000 . . . . . . . . 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 1187 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  Y ) )  e.  B )
422, 23opoccl 28288 . . . . . . . . . 10  |-  ( ( K  e.  OP  /\  Z  e.  B )  ->  ( ( oc `  K ) `  Z
)  e.  B )
4335, 12, 42syl2anc 645 . . . . . . . . 9  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  Z )  e.  B )
442, 4latjcl 14000 . . . . . . . . 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 1187 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  Z ) )  e.  B )
462, 5latmcl 14001 . . . . . . . 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 1187 . . . . . . 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 28323 . . . . . . 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 1189 . . . . . 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 980 . . . . 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 28344 . . . . . . . . . . . . 13  |-  ( ( K  e.  OML  /\  X  e.  B  /\  Y  e.  B )  ->  ( X C Y  <-> 
X C ( ( oc `  K ) `
 Y ) ) )
53523adant3r3 1167 . . . . . . . . . . . 12  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X C Y  <->  X C
( ( oc `  K ) `  Y
) ) )
54 simpl 445 . . . . . . . . . . . . 13  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  OML )
552, 4, 5, 23, 51cmtbr3N 28348 . . . . . . . . . . . . 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 1187 . . . . . . . . . . . 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 246 . . . . . . . . . . 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 472 . . . . . . . . . 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 700 . . . . . . . . 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 1151 . . . . . . . 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 28344 . . . . . . . . . . . . 13  |-  ( ( K  e.  OML  /\  X  e.  B  /\  Z  e.  B )  ->  ( X C Z  <-> 
X C ( ( oc `  K ) `
 Z ) ) )
62613adant3r2 1166 . . . . . . . . . . . 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 28348 . . . . . . . . . . . . 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 1187 . . . . . . . . . . . 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 246 . . . . . . . . . . 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 472 . . . . . . . . . 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 699 . . . . . . . . 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 1151 . . . . . . . 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 5728 . . . . . . 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 28328 . . . . . . . . 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 1189 . . . . . . . 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 980 . . . . . . 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 28328 . . . . . . . . 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 1189 . . . . . . . 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 980 . . . . . . 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 2295 . . . . . 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 5726 . . . . 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 14001 . . . . . . . 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 1187 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( ( oc `  K ) `  Y
)  ./\  ( ( oc `  K ) `  Z ) )  e.  B )
802, 5latm12 28324 . . . . . . 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 1189 . . . . . 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 980 . . . . 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 2289 . . . 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 28315 . . . . . . . . . 10  |-  ( ( K  e.  OL  /\  Y  e.  B  /\  Z  e.  B )  ->  ( ( oc `  K ) `  ( Y  .\/  Z ) )  =  ( ( ( oc `  K ) `
 Y )  ./\  ( ( oc `  K ) `  Z
) ) )
8518, 11, 12, 84syl3anc 1187 . . . . . . . . 9  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( oc `  K
) `  ( Y  .\/  Z ) )  =  ( ( ( oc
`  K ) `  Y )  ./\  (
( oc `  K
) `  Z )
) )
8685oveq2d 5726 . . . . . . . 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 2253 . . . . . . . . . 10  |-  ( 0.
`  K )  =  ( 0. `  K
)
882, 23, 5, 87opnoncon 28302 . . . . . . . . 9  |-  ( ( K  e.  OP  /\  ( Y  .\/  Z )  e.  B )  -> 
( ( Y  .\/  Z )  ./\  ( ( oc `  K ) `  ( Y  .\/  Z ) ) )  =  ( 0. `  K ) )
8935, 14, 88syl2anc 645 . . . . . . . 8  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( Y  .\/  Z
)  ./\  ( ( oc `  K ) `  ( Y  .\/  Z ) ) )  =  ( 0. `  K ) )
9086, 89eqtr3d 2287 . . . . . . 7  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( Y  .\/  Z
)  ./\  ( (
( oc `  K
) `  Y )  ./\  ( ( oc `  K ) `  Z
) ) )  =  ( 0. `  K
) )
9190oveq2d 5726 . . . . . 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 28330 . . . . . . 7  |-  ( ( K  e.  OL  /\  X  e.  B )  ->  ( X  ./\  ( 0. `  K ) )  =  ( 0. `  K ) )
9318, 10, 92syl2anc 645 . . . . . 6  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  ( 0. `  K ) )  =  ( 0. `  K
) )
9491, 93eqtrd 2285 . . . . 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 980 . . . 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 2289 . . 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 14000 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( X  ./\  Y )  e.  B  /\  ( X  ./\  Z )  e.  B )  ->  (
( X  ./\  Y
)  .\/  ( X  ./\ 
Z ) )  e.  B )
989, 20, 22, 97syl3anc 1187 . . . . 5  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  ./\  Y
)  .\/  ( X  ./\ 
Z ) )  e.  B )
992, 5latmcl 14001 . . . . . 6  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( Y  .\/  Z )  e.  B )  -> 
( X  ./\  ( Y  .\/  Z ) )  e.  B )
1009, 10, 14, 99syl3anc 1187 . . . . 5  |-  ( ( K  e.  OML  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  ./\  ( Y  .\/  Z ) )  e.  B
)
1012, 3, 5, 23, 87omllaw3 28339 . . . . 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 1187 . . . 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 980 . . 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 663 . 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 2258 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 6    <-> wb 178    /\ wa 360    /\ w3a 939    = wceq 1619    e. wcel 1621   class class class wbr 3920   ` cfv 4592  (class class class)co 5710   Basecbs 13022   lecple 13089   occoc 13090   joincjn 13922   meetcmee 13923   0.cp0 13987   Latclat 13995   OPcops 28266   cmccmtN 28267   OLcol 28268   OMLcoml 28269
This theorem is referenced by:  omlfh3N  28353  omlmod1i2N  28354
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-rep 4028  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-nel 2415  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-iun 3805  df-br 3921  df-opab 3975  df-mpt 3976  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fo 4606  df-f1o 4607  df-fv 4608  df-ov 5713  df-oprab 5714  df-mpt2 5715  df-1st 5974  df-2nd 5975  df-iota 6143  df-undef 6182  df-riota 6190  df-poset 13924  df-lub 13952  df-glb 13953  df-join 13954  df-meet 13955  df-p0 13989  df-lat 13996  df-oposet 28270  df-cmtN 28271  df-ol 28272  df-oml 28273
  Copyright terms: Public domain W3C validator