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

Theorem cvrat4 30079
Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in [PtakPulmannova] p. 68. Also Lemma 9.2(delta) in [MaedaMaeda] p. 41. (atcvat4i 23888 analog.) (Contributed by NM, 30-Nov-2011.)
Hypotheses
Ref Expression
cvrat4.b  |-  B  =  ( Base `  K
)
cvrat4.l  |-  .<_  =  ( le `  K )
cvrat4.j  |-  .\/  =  ( join `  K )
cvrat4.z  |-  .0.  =  ( 0. `  K )
cvrat4.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
cvrat4  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( X  =/=  .0.  /\  P  .<_  ( X  .\/  Q ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) )
Distinct variable groups:    A, r    B, r    .\/ , r    K, r    .<_ , r    P, r    Q, r    X, r
Allowed substitution hint:    .0. ( r)

Proof of Theorem cvrat4
StepHypRef Expression
1 hlatl 29997 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  AtLat )
21adantr 452 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  K  e.  AtLat )
3 simpr1 963 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  X  e.  B )
4 cvrat4.b . . . . . . . . . . 11  |-  B  =  ( Base `  K
)
5 cvrat4.l . . . . . . . . . . 11  |-  .<_  =  ( le `  K )
6 cvrat4.z . . . . . . . . . . 11  |-  .0.  =  ( 0. `  K )
7 cvrat4.a . . . . . . . . . . 11  |-  A  =  ( Atoms `  K )
84, 5, 6, 7atlex 29953 . . . . . . . . . 10  |-  ( ( K  e.  AtLat  /\  X  e.  B  /\  X  =/= 
.0.  )  ->  E. r  e.  A  r  .<_  X )
983exp 1152 . . . . . . . . 9  |-  ( K  e.  AtLat  ->  ( X  e.  B  ->  ( X  =/=  .0.  ->  E. r  e.  A  r  .<_  X ) ) )
102, 3, 9sylc 58 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X  =/=  .0.  ->  E. r  e.  A  r  .<_  X ) )
1110adantr 452 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  P  =  Q )  ->  ( X  =/=  .0.  ->  E. r  e.  A  r  .<_  X ) )
12 simpll 731 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  r  e.  A )  ->  K  e.  HL )
13 simplr3 1001 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  r  e.  A )  ->  Q  e.  A )
14 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  r  e.  A )  ->  r  e.  A )
15 cvrat4.j . . . . . . . . . . . . . . 15  |-  .\/  =  ( join `  K )
165, 15, 7hlatlej1 30011 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  Q  e.  A  /\  r  e.  A )  ->  Q  .<_  ( Q  .\/  r ) )
1712, 13, 14, 16syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  r  e.  A )  ->  Q  .<_  ( Q  .\/  r
) )
18 breq1 4207 . . . . . . . . . . . . 13  |-  ( P  =  Q  ->  ( P  .<_  ( Q  .\/  r )  <->  Q  .<_  ( Q  .\/  r ) ) )
1917, 18syl5ibr 213 . . . . . . . . . . . 12  |-  ( P  =  Q  ->  (
( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A ) )  /\  r  e.  A )  ->  P  .<_  ( Q  .\/  r ) ) )
2019exp3a 426 . . . . . . . . . . 11  |-  ( P  =  Q  ->  (
( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
r  e.  A  ->  P  .<_  ( Q  .\/  r ) ) ) )
2120impcom 420 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  P  =  Q )  ->  (
r  e.  A  ->  P  .<_  ( Q  .\/  r ) ) )
2221anim2d 549 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  P  =  Q )  ->  (
( r  .<_  X  /\  r  e.  A )  ->  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) )
2322exp3acom23 1381 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  P  =  Q )  ->  (
r  e.  A  -> 
( r  .<_  X  -> 
( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) )
2423reximdvai 2808 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  P  =  Q )  ->  ( E. r  e.  A  r  .<_  X  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) )
2511, 24syld 42 . . . . . 6  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  P  =  Q )  ->  ( X  =/=  .0.  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) )
2625ex 424 . . . . 5  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( P  =  Q  ->  ( X  =/=  .0.  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) )
2726a1i 11 . . . 4  |-  ( P 
.<_  ( X  .\/  Q
)  ->  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A )
)  ->  ( P  =  Q  ->  ( X  =/=  .0.  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) ) )
2827com4l 80 . . 3  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( P  =  Q  ->  ( X  =/=  .0.  ->  ( P  .<_  ( X  .\/  Q )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) ) )
2928imp4a 573 . 2  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( P  =  Q  ->  ( ( X  =/=  .0.  /\  P  .<_  ( X  .\/  Q ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) )
30 hllat 30000 . . . . . . . . . . . . . 14  |-  ( K  e.  HL  ->  K  e.  Lat )
3130adantr 452 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  K  e.  Lat )
32 simpr3 965 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  Q  e.  A )
334, 7atbase 29926 . . . . . . . . . . . . . 14  |-  ( Q  e.  A  ->  Q  e.  B )
3432, 33syl 16 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  Q  e.  B )
354, 5, 15latleeqj2 14481 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  Q  e.  B  /\  X  e.  B )  ->  ( Q  .<_  X  <->  ( X  .\/  Q )  =  X ) )
3631, 34, 3, 35syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( Q  .<_  X  <->  ( X  .\/  Q )  =  X ) )
3736biimpa 471 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  Q  .<_  X )  ->  ( X  .\/  Q )  =  X )
3837breq2d 4216 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  Q  .<_  X )  ->  ( P  .<_  ( X  .\/  Q )  <->  P  .<_  X ) )
3938biimpa 471 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A ) )  /\  Q  .<_  X )  /\  P  .<_  ( X  .\/  Q ) )  ->  P  .<_  X )
4039expl 602 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( Q  .<_  X  /\  P  .<_  ( X  .\/  Q ) )  ->  P  .<_  X ) )
41 simpl 444 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  K  e.  HL )
42 simpr2 964 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  P  e.  A )
435, 15, 7hlatlej2 30012 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  Q  e.  A  /\  P  e.  A )  ->  P  .<_  ( Q  .\/  P ) )
4441, 32, 42, 43syl3anc 1184 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  P  .<_  ( Q  .\/  P
) )
4540, 44jctird 529 . . . . . . 7  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( Q  .<_  X  /\  P  .<_  ( X  .\/  Q ) )  ->  ( P  .<_  X  /\  P  .<_  ( Q  .\/  P
) ) ) )
4645, 42jctild 528 . . . . . 6  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( Q  .<_  X  /\  P  .<_  ( X  .\/  Q ) )  ->  ( P  e.  A  /\  ( P  .<_  X  /\  P  .<_  ( Q  .\/  P ) ) ) ) )
4746impl 604 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A ) )  /\  Q  .<_  X )  /\  P  .<_  ( X  .\/  Q ) )  ->  ( P  e.  A  /\  ( P  .<_  X  /\  P  .<_  ( Q  .\/  P ) ) ) )
48 breq1 4207 . . . . . . 7  |-  ( r  =  P  ->  (
r  .<_  X  <->  P  .<_  X ) )
49 oveq2 6080 . . . . . . . 8  |-  ( r  =  P  ->  ( Q  .\/  r )  =  ( Q  .\/  P
) )
5049breq2d 4216 . . . . . . 7  |-  ( r  =  P  ->  ( P  .<_  ( Q  .\/  r )  <->  P  .<_  ( Q  .\/  P ) ) )
5148, 50anbi12d 692 . . . . . 6  |-  ( r  =  P  ->  (
( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) )  <->  ( P  .<_  X  /\  P  .<_  ( Q  .\/  P ) ) ) )
5251rspcev 3044 . . . . 5  |-  ( ( P  e.  A  /\  ( P  .<_  X  /\  P  .<_  ( Q  .\/  P ) ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) )
5347, 52syl 16 . . . 4  |-  ( ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A ) )  /\  Q  .<_  X )  /\  P  .<_  ( X  .\/  Q ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) )
5453adantrl 697 . . 3  |-  ( ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A ) )  /\  Q  .<_  X )  /\  ( X  =/=  .0.  /\  P  .<_  ( X  .\/  Q ) ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) )
5554exp31 588 . 2  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( Q  .<_  X  ->  (
( X  =/=  .0.  /\  P  .<_  ( X  .\/  Q ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) )
56 simpr 448 . . 3  |-  ( ( X  =/=  .0.  /\  P  .<_  ( X  .\/  Q ) )  ->  P  .<_  ( X  .\/  Q
) )
57 ioran 477 . . . . 5  |-  ( -.  ( P  =  Q  \/  Q  .<_  X )  <-> 
( -.  P  =  Q  /\  -.  Q  .<_  X ) )
58 df-ne 2600 . . . . . 6  |-  ( P  =/=  Q  <->  -.  P  =  Q )
5958anbi1i 677 . . . . 5  |-  ( ( P  =/=  Q  /\  -.  Q  .<_  X )  <-> 
( -.  P  =  Q  /\  -.  Q  .<_  X ) )
6057, 59bitr4i 244 . . . 4  |-  ( -.  ( P  =  Q  \/  Q  .<_  X )  <-> 
( P  =/=  Q  /\  -.  Q  .<_  X ) )
61 eqid 2435 . . . . . . . . . 10  |-  ( meet `  K )  =  (
meet `  K )
624, 5, 15, 61, 7cvrat3 30078 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( P  =/=  Q  /\  -.  Q  .<_  X  /\  P  .<_  ( X  .\/  Q ) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  e.  A
) )
63623expd 1170 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( P  =/=  Q  ->  ( -.  Q  .<_  X  -> 
( P  .<_  ( X 
.\/  Q )  -> 
( X ( meet `  K ) ( P 
.\/  Q ) )  e.  A ) ) ) )
6463imp4c 575 . . . . . . 7  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( ( P  =/= 
Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X  .\/  Q
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  e.  A
) )
654, 7atbase 29926 . . . . . . . . . . . . 13  |-  ( P  e.  A  ->  P  e.  B )
6642, 65syl 16 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  P  e.  B )
674, 15latjcl 14467 . . . . . . . . . . . 12  |-  ( ( K  e.  Lat  /\  P  e.  B  /\  Q  e.  B )  ->  ( P  .\/  Q
)  e.  B )
6831, 66, 34, 67syl3anc 1184 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( P  .\/  Q )  e.  B )
694, 5, 61latmle1 14493 . . . . . . . . . . 11  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( P  .\/  Q )  e.  B )  -> 
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  X )
7031, 3, 68, 69syl3anc 1184 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  X )
7170adantr 452 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  ( X
( meet `  K )
( P  .\/  Q
) )  .<_  X )
72 simpll 731 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  K  e.  HL )
7363imp44 580 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  ( X
( meet `  K )
( P  .\/  Q
) )  e.  A
)
74 simplr2 1000 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  P  e.  A )
7534adantr 452 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  Q  e.  B )
7673, 74, 753jca 1134 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  ( ( X ( meet `  K
) ( P  .\/  Q ) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )
7772, 76jca 519 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  ( K  e.  HL  /\  ( ( X ( meet `  K
) ( P  .\/  Q ) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) ) )
784, 5, 61, 6, 7atnle 29954 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  AtLat  /\  Q  e.  A  /\  X  e.  B )  ->  ( -.  Q  .<_  X  <->  ( Q
( meet `  K ) X )  =  .0.  ) )
792, 32, 3, 78syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( -.  Q  .<_  X  <->  ( Q
( meet `  K ) X )  =  .0.  ) )
804, 61latmcom 14492 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Lat  /\  Q  e.  B  /\  X  e.  B )  ->  ( Q ( meet `  K ) X )  =  ( X (
meet `  K ) Q ) )
8131, 34, 3, 80syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( Q ( meet `  K
) X )  =  ( X ( meet `  K ) Q ) )
8281eqeq1d 2443 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( Q ( meet `  K ) X )  =  .0.  <->  ( X
( meet `  K ) Q )  =  .0.  ) )
8379, 82bitrd 245 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( -.  Q  .<_  X  <->  ( X
( meet `  K ) Q )  =  .0.  ) )
844, 61latmcl 14468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( P  .\/  Q )  e.  B )  -> 
( X ( meet `  K ) ( P 
.\/  Q ) )  e.  B )
8531, 3, 68, 84syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  e.  B
)
8685, 3, 343jca 1134 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( X ( meet `  K ) ( P 
.\/  Q ) )  e.  B  /\  X  e.  B  /\  Q  e.  B ) )
8731, 86jca 519 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( K  e.  Lat  /\  (
( X ( meet `  K ) ( P 
.\/  Q ) )  e.  B  /\  X  e.  B  /\  Q  e.  B ) ) )
884, 5, 61latmlem2 14499 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  Lat  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  B  /\  X  e.  B  /\  Q  e.  B
) )  ->  (
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  X  ->  ( Q
( meet `  K )
( X ( meet `  K ) ( P 
.\/  Q ) ) )  .<_  ( Q
( meet `  K ) X ) ) )
8987, 70, 88sylc 58 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( Q ( meet `  K
) ( X (
meet `  K )
( P  .\/  Q
) ) )  .<_  ( Q ( meet `  K
) X ) )
9089, 81breqtrd 4228 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( Q ( meet `  K
) ( X (
meet `  K )
( P  .\/  Q
) ) )  .<_  ( X ( meet `  K
) Q ) )
91 breq2 4208 . . . . . . . . . . . . . . . 16  |-  ( ( X ( meet `  K
) Q )  =  .0.  ->  ( ( Q ( meet `  K
) ( X (
meet `  K )
( P  .\/  Q
) ) )  .<_  ( X ( meet `  K
) Q )  <->  ( Q
( meet `  K )
( X ( meet `  K ) ( P 
.\/  Q ) ) )  .<_  .0.  )
)
9290, 91syl5ibcom 212 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( X ( meet `  K ) Q )  =  .0.  ->  ( Q ( meet `  K
) ( X (
meet `  K )
( P  .\/  Q
) ) )  .<_  .0.  ) )
93 hlop 29999 . . . . . . . . . . . . . . . . 17  |-  ( K  e.  HL  ->  K  e.  OP )
9493adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  K  e.  OP )
954, 61latmcl 14468 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Lat  /\  Q  e.  B  /\  ( X ( meet `  K
) ( P  .\/  Q ) )  e.  B
)  ->  ( Q
( meet `  K )
( X ( meet `  K ) ( P 
.\/  Q ) ) )  e.  B )
9631, 34, 85, 95syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( Q ( meet `  K
) ( X (
meet `  K )
( P  .\/  Q
) ) )  e.  B )
974, 5, 6ople0 29824 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  OP  /\  ( Q ( meet `  K
) ( X (
meet `  K )
( P  .\/  Q
) ) )  e.  B )  ->  (
( Q ( meet `  K ) ( X ( meet `  K
) ( P  .\/  Q ) ) )  .<_  .0. 
<->  ( Q ( meet `  K ) ( X ( meet `  K
) ( P  .\/  Q ) ) )  =  .0.  ) )
9894, 96, 97syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( Q ( meet `  K ) ( X ( meet `  K
) ( P  .\/  Q ) ) )  .<_  .0. 
<->  ( Q ( meet `  K ) ( X ( meet `  K
) ( P  .\/  Q ) ) )  =  .0.  ) )
9992, 98sylibd 206 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( X ( meet `  K ) Q )  =  .0.  ->  ( Q ( meet `  K
) ( X (
meet `  K )
( P  .\/  Q
) ) )  =  .0.  ) )
10083, 99sylbid 207 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( -.  Q  .<_  X  -> 
( Q ( meet `  K ) ( X ( meet `  K
) ( P  .\/  Q ) ) )  =  .0.  ) )
101100imp 419 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  -.  Q  .<_  X )  -> 
( Q ( meet `  K ) ( X ( meet `  K
) ( P  .\/  Q ) ) )  =  .0.  )
102101adantrl 697 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  ( P  =/=  Q  /\  -.  Q  .<_  X ) )  ->  ( Q (
meet `  K )
( X ( meet `  K ) ( P 
.\/  Q ) ) )  =  .0.  )
103102adantrr 698 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  ( Q
( meet `  K )
( X ( meet `  K ) ( P 
.\/  Q ) ) )  =  .0.  )
1044, 5, 61latmle2 14494 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( P  .\/  Q )  e.  B )  -> 
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  ( P  .\/  Q
) )
10531, 3, 68, 104syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  ( P 
.\/  Q ) )
1064, 15latjcom 14476 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  P  e.  B  /\  Q  e.  B )  ->  ( P  .\/  Q
)  =  ( Q 
.\/  P ) )
10731, 66, 34, 106syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( P  .\/  Q )  =  ( Q  .\/  P
) )
108105, 107breqtrd 4228 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  ( Q 
.\/  P ) )
109108adantr 452 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  ( X
( meet `  K )
( P  .\/  Q
) )  .<_  ( Q 
.\/  P ) )
11030adantr 452 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  K  e.  Lat )
111 simpr3 965 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  Q  e.  B )
112 simpr1 963 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  e.  A
)
1134, 7atbase 29926 . . . . . . . . . . . . . 14  |-  ( ( X ( meet `  K
) ( P  .\/  Q ) )  e.  A  ->  ( X ( meet `  K ) ( P 
.\/  Q ) )  e.  B )
114112, 113syl 16 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  e.  B
)
1154, 61latmcom 14492 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  Q  e.  B  /\  ( X ( meet `  K
) ( P  .\/  Q ) )  e.  B
)  ->  ( Q
( meet `  K )
( X ( meet `  K ) ( P 
.\/  Q ) ) )  =  ( ( X ( meet `  K
) ( P  .\/  Q ) ) ( meet `  K ) Q ) )
116110, 111, 114, 115syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  ( Q ( meet `  K
) ( X (
meet `  K )
( P  .\/  Q
) ) )  =  ( ( X (
meet `  K )
( P  .\/  Q
) ) ( meet `  K ) Q ) )
117116eqeq1d 2443 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  (
( Q ( meet `  K ) ( X ( meet `  K
) ( P  .\/  Q ) ) )  =  .0.  <->  ( ( X ( meet `  K
) ( P  .\/  Q ) ) ( meet `  K ) Q )  =  .0.  ) )
1184, 5, 15, 61, 6, 7hlexch3 30027 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
)  /\  ( ( X ( meet `  K
) ( P  .\/  Q ) ) ( meet `  K ) Q )  =  .0.  )  -> 
( ( X (
meet `  K )
( P  .\/  Q
) )  .<_  ( Q 
.\/  P )  ->  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) )
1191183expia 1155 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  (
( ( X (
meet `  K )
( P  .\/  Q
) ) ( meet `  K ) Q )  =  .0.  ->  (
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  ( Q  .\/  P
)  ->  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) ) )
120117, 119sylbid 207 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  (
( Q ( meet `  K ) ( X ( meet `  K
) ( P  .\/  Q ) ) )  =  .0.  ->  ( ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  ( Q 
.\/  P )  ->  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) ) )
12177, 103, 109, 120syl3c 59 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) )
12271, 121jca 519 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  ( ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  X  /\  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) )
123122ex 424 . . . . . . 7  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( ( P  =/= 
Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X  .\/  Q
) )  ->  (
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  X  /\  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) ) )
12464, 123jcad 520 . . . . . 6  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( ( P  =/= 
Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X  .\/  Q
) )  ->  (
( X ( meet `  K ) ( P 
.\/  Q ) )  e.  A  /\  (
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  X  /\  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) ) ) )
125 breq1 4207 . . . . . . . 8  |-  ( r  =  ( X (
meet `  K )
( P  .\/  Q
) )  ->  (
r  .<_  X  <->  ( X
( meet `  K )
( P  .\/  Q
) )  .<_  X ) )
126 oveq2 6080 . . . . . . . . 9  |-  ( r  =  ( X (
meet `  K )
( P  .\/  Q
) )  ->  ( Q  .\/  r )  =  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) )
127126breq2d 4216 . . . . . . . 8  |-  ( r  =  ( X (
meet `  K )
( P  .\/  Q
) )  ->  ( P  .<_  ( Q  .\/  r )  <->  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) )
128125, 127anbi12d 692 . . . . . . 7  |-  ( r  =  ( X (
meet `  K )
( P  .\/  Q
) )  ->  (
( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) )  <->  ( ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  X  /\  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) ) )
129128rspcev 3044 . . . . . 6  |-  ( ( ( X ( meet `  K ) ( P 
.\/  Q ) )  e.  A  /\  (
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  X  /\  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) )
130124, 129syl6 31 . . . . 5  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( ( P  =/= 
Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X  .\/  Q
) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) )
131130exp3a 426 . . . 4  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( P  =/=  Q  /\  -.  Q  .<_  X )  ->  ( P  .<_  ( X  .\/  Q )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) )
13260, 131syl5bi 209 . . 3  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( -.  ( P  =  Q  \/  Q  .<_  X )  ->  ( P  .<_  ( X  .\/  Q )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) )
13356, 132syl7 65 . 2  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( -.  ( P  =  Q  \/  Q  .<_  X )  ->  ( ( X  =/=  .0.  /\  P  .<_  ( X  .\/  Q
) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) ) )
13429, 55, 133ecase3d 910 1  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( X  =/=  .0.  /\  P  .<_  ( X  .\/  Q ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    /\ w3a 936    = wceq 1652    e. wcel 1725    =/= wne 2598   E.wrex 2698   class class class wbr 4204   ` cfv 5445  (class class class)co 6072   Basecbs 13457   lecple 13524   joincjn 14389   meetcmee 14390   0.cp0 14454   Latclat 14462   OPcops 29809   Atomscatm 29900   AtLatcal 29901   HLchlt 29987
This theorem is referenced by:  cvrat42  30080  ps-2  30114
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-1st 6340  df-2nd 6341  df-undef 6534  df-riota 6540  df-poset 14391  df-plt 14403  df-lub 14419  df-glb 14420  df-join 14421  df-meet 14422  df-p0 14456  df-lat 14463  df-clat 14525  df-oposet 29813  df-ol 29815  df-oml 29816  df-covers 29903  df-ats 29904  df-atl 29935  df-cvlat 29959  df-hlat 29988
  Copyright terms: Public domain W3C validator