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

Theorem cvrat4 30254
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 22993 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 30172 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  AtLat )
21adantr 451 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  K  e.  AtLat )
3 simpr1 961 . . . . . . . . 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 30128 . . . . . . . . . 10  |-  ( ( K  e.  AtLat  /\  X  e.  B  /\  X  =/= 
.0.  )  ->  E. r  e.  A  r  .<_  X )
983exp 1150 . . . . . . . . 9  |-  ( K  e.  AtLat  ->  ( X  e.  B  ->  ( X  =/=  .0.  ->  E. r  e.  A  r  .<_  X ) ) )
102, 3, 9sylc 56 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X  =/=  .0.  ->  E. r  e.  A  r  .<_  X ) )
1110adantr 451 . . . . . . 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 730 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  r  e.  A )  ->  K  e.  HL )
13 simplr3 999 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  r  e.  A )  ->  Q  e.  A )
14 simpr 447 . . . . . . . . . . . . . 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 30186 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  Q  e.  A  /\  r  e.  A )  ->  Q  .<_  ( Q  .\/  r ) )
1712, 13, 14, 16syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  r  e.  A )  ->  Q  .<_  ( Q  .\/  r
) )
18 breq1 4042 . . . . . . . . . . . . 13  |-  ( P  =  Q  ->  ( P  .<_  ( Q  .\/  r )  <->  Q  .<_  ( Q  .\/  r ) ) )
1917, 18syl5ibr 212 . . . . . . . . . . . 12  |-  ( P  =  Q  ->  (
( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A ) )  /\  r  e.  A )  ->  P  .<_  ( Q  .\/  r ) ) )
2019exp3a 425 . . . . . . . . . . 11  |-  ( P  =  Q  ->  (
( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
r  e.  A  ->  P  .<_  ( Q  .\/  r ) ) ) )
2120impcom 419 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  P  =  Q )  ->  (
r  e.  A  ->  P  .<_  ( Q  .\/  r ) ) )
2221anim2d 548 . . . . . . . . 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 1362 . . . . . . . 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 2666 . . . . . . 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 40 . . . . . 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 423 . . . . 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 10 . . . 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 78 . . 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 572 . 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 30175 . . . . . . . . . . . . . 14  |-  ( K  e.  HL  ->  K  e.  Lat )
3130adantr 451 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  K  e.  Lat )
32 simpr3 963 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  Q  e.  A )
334, 7atbase 30101 . . . . . . . . . . . . . 14  |-  ( Q  e.  A  ->  Q  e.  B )
3432, 33syl 15 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  Q  e.  B )
354, 5, 15latleeqj2 14186 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  Q  e.  B  /\  X  e.  B )  ->  ( Q  .<_  X  <->  ( X  .\/  Q )  =  X ) )
3631, 34, 3, 35syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( Q  .<_  X  <->  ( X  .\/  Q )  =  X ) )
3736biimpa 470 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  Q  .<_  X )  ->  ( X  .\/  Q )  =  X )
3837breq2d 4051 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  Q  .<_  X )  ->  ( P  .<_  ( X  .\/  Q )  <->  P  .<_  X ) )
3938biimpa 470 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A ) )  /\  Q  .<_  X )  /\  P  .<_  ( X  .\/  Q ) )  ->  P  .<_  X )
4039expl 601 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  (
( Q  .<_  X  /\  P  .<_  ( X  .\/  Q ) )  ->  P  .<_  X ) )
41 simpl 443 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  K  e.  HL )
42 simpr2 962 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  P  e.  A )
435, 15, 7hlatlej2 30187 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  Q  e.  A  /\  P  e.  A )  ->  P  .<_  ( Q  .\/  P ) )
4441, 32, 42, 43syl3anc 1182 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  P  .<_  ( Q  .\/  P
) )
4540, 44jctird 528 . . . . . . 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 527 . . . . . 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 603 . . . . 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 4042 . . . . . . 7  |-  ( r  =  P  ->  (
r  .<_  X  <->  P  .<_  X ) )
49 oveq2 5882 . . . . . . . 8  |-  ( r  =  P  ->  ( Q  .\/  r )  =  ( Q  .\/  P
) )
5049breq2d 4051 . . . . . . 7  |-  ( r  =  P  ->  ( P  .<_  ( Q  .\/  r )  <->  P  .<_  ( Q  .\/  P ) ) )
5148, 50anbi12d 691 . . . . . 6  |-  ( r  =  P  ->  (
( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) )  <->  ( P  .<_  X  /\  P  .<_  ( Q  .\/  P ) ) ) )
5251rspcev 2897 . . . . 5  |-  ( ( P  e.  A  /\  ( P  .<_  X  /\  P  .<_  ( Q  .\/  P ) ) )  ->  E. r  e.  A  ( r  .<_  X  /\  P  .<_  ( Q  .\/  r ) ) )
5347, 52syl 15 . . . 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 696 . . 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 587 . 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 447 . . 3  |-  ( ( X  =/=  .0.  /\  P  .<_  ( X  .\/  Q ) )  ->  P  .<_  ( X  .\/  Q
) )
57 ioran 476 . . . . 5  |-  ( -.  ( P  =  Q  \/  Q  .<_  X )  <-> 
( -.  P  =  Q  /\  -.  Q  .<_  X ) )
58 df-ne 2461 . . . . . 6  |-  ( P  =/=  Q  <->  -.  P  =  Q )
5958anbi1i 676 . . . . 5  |-  ( ( P  =/=  Q  /\  -.  Q  .<_  X )  <-> 
( -.  P  =  Q  /\  -.  Q  .<_  X ) )
6057, 59bitr4i 243 . . . 4  |-  ( -.  ( P  =  Q  \/  Q  .<_  X )  <-> 
( P  =/=  Q  /\  -.  Q  .<_  X ) )
61 eqid 2296 . . . . . . . . . 10  |-  ( meet `  K )  =  (
meet `  K )
624, 5, 15, 61, 7cvrat3 30253 . . . . . . . . 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 1168 . . . . . . . 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 574 . . . . . . 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 30101 . . . . . . . . . . . . 13  |-  ( P  e.  A  ->  P  e.  B )
6642, 65syl 15 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  P  e.  B )
674, 15latjcl 14172 . . . . . . . . . . . 12  |-  ( ( K  e.  Lat  /\  P  e.  B  /\  Q  e.  B )  ->  ( P  .\/  Q
)  e.  B )
6831, 66, 34, 67syl3anc 1182 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( P  .\/  Q )  e.  B )
694, 5, 61latmle1 14198 . . . . . . . . . . 11  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( P  .\/  Q )  e.  B )  -> 
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  X )
7031, 3, 68, 69syl3anc 1182 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  X )
7170adantr 451 . . . . . . . . 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 730 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  K  e.  HL )
7363imp44 579 . . . . . . . . . . . 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 998 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  /\  (
( P  =/=  Q  /\  -.  Q  .<_  X )  /\  P  .<_  ( X 
.\/  Q ) ) )  ->  P  e.  A )
7534adantr 451 . . . . . . . . . . . 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 1132 . . . . . . . . . . 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 518 . . . . . . . . . 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 30129 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  AtLat  /\  Q  e.  A  /\  X  e.  B )  ->  ( -.  Q  .<_  X  <->  ( Q
( meet `  K ) X )  =  .0.  ) )
792, 32, 3, 78syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( -.  Q  .<_  X  <->  ( Q
( meet `  K ) X )  =  .0.  ) )
804, 61latmcom 14197 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Lat  /\  Q  e.  B  /\  X  e.  B )  ->  ( Q ( meet `  K ) X )  =  ( X (
meet `  K ) Q ) )
8131, 34, 3, 80syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( Q ( meet `  K
) X )  =  ( X ( meet `  K ) Q ) )
8281eqeq1d 2304 . . . . . . . . . . . . . . 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 244 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( -.  Q  .<_  X  <->  ( X
( meet `  K ) Q )  =  .0.  ) )
844, 61latmcl 14173 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( P  .\/  Q )  e.  B )  -> 
( X ( meet `  K ) ( P 
.\/  Q ) )  e.  B )
8531, 3, 68, 84syl3anc 1182 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  e.  B
)
8685, 3, 343jca 1132 . . . . . . . . . . . . . . . . . . 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 518 . . . . . . . . . . . . . . . . . 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 14204 . . . . . . . . . . . . . . . . . 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 56 . . . . . . . . . . . . . . . . 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 4063 . . . . . . . . . . . . . . . 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 4043 . . . . . . . . . . . . . . . 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 211 . . . . . . . . . . . . . . 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 30174 . . . . . . . . . . . . . . . . 17  |-  ( K  e.  HL  ->  K  e.  OP )
9493adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  K  e.  OP )
954, 61latmcl 14173 . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . 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 29999 . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . 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 205 . . . . . . . . . . . . . 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 206 . . . . . . . . . . . . 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 418 . . . . . . . . . . . 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 696 . . . . . . . . . . 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 697 . . . . . . . . . 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 14199 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  ( P  .\/  Q )  e.  B )  -> 
( X ( meet `  K ) ( P 
.\/  Q ) ) 
.<_  ( P  .\/  Q
) )
10531, 3, 68, 104syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  ( P 
.\/  Q ) )
1064, 15latjcom 14181 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  P  e.  B  /\  Q  e.  B )  ->  ( P  .\/  Q
)  =  ( Q 
.\/  P ) )
10731, 66, 34, 106syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( P  .\/  Q )  =  ( Q  .\/  P
) )
108105, 107breqtrd 4063 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( X  e.  B  /\  P  e.  A  /\  Q  e.  A
) )  ->  ( X ( meet `  K
) ( P  .\/  Q ) )  .<_  ( Q 
.\/  P ) )
109108adantr 451 . . . . . . . . . 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 451 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  K  e.  Lat )
111 simpr3 963 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( ( X (
meet `  K )
( P  .\/  Q
) )  e.  A  /\  P  e.  A  /\  Q  e.  B
) )  ->  Q  e.  B )
112 simpr1 961 . . . . . . . . . . . . . 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 30101 . . . . . . . . . . . . . 14  |-  ( ( X ( meet `  K
) ( P  .\/  Q ) )  e.  A  ->  ( X ( meet `  K ) ( P 
.\/  Q ) )  e.  B )
114112, 113syl 15 . . . . . . . . . . . . 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 14197 . . . . . . . . . . . . 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 1182 . . . . . . . . . . . 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 2304 . . . . . . . . . . 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 30202 . . . . . . . . . . . 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 1153 . . . . . . . . . . 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 206 . . . . . . . . . 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 57 . . . . . . . . 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 518 . . . . . . . 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 423 . . . . . . 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 519 . . . . . 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 4042 . . . . . . . 8  |-  ( r  =  ( X (
meet `  K )
( P  .\/  Q
) )  ->  (
r  .<_  X  <->  ( X
( meet `  K )
( P  .\/  Q
) )  .<_  X ) )
126 oveq2 5882 . . . . . . . . 9  |-  ( r  =  ( X (
meet `  K )
( P  .\/  Q
) )  ->  ( Q  .\/  r )  =  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) )
127126breq2d 4051 . . . . . . . 8  |-  ( r  =  ( X (
meet `  K )
( P  .\/  Q
) )  ->  ( P  .<_  ( Q  .\/  r )  <->  P  .<_  ( Q  .\/  ( X ( meet `  K
) ( P  .\/  Q ) ) ) ) )
128125, 127anbi12d 691 . . . . . . 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 2897 . . . . . 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 29 . . . . 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 425 . . . 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 208 . . 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 63 . 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 909 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 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696    =/= wne 2459   E.wrex 2557   class class class wbr 4039   ` cfv 5271  (class class class)co 5874   Basecbs 13164   lecple 13231   joincjn 14094   meetcmee 14095   0.cp0 14159   Latclat 14167   OPcops 29984   Atomscatm 30075   AtLatcal 30076   HLchlt 30162
This theorem is referenced by:  cvrat42  30255  ps-2  30289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-undef 6314  df-riota 6320  df-poset 14096  df-plt 14108  df-lub 14124  df-glb 14125  df-join 14126  df-meet 14127  df-p0 14161  df-lat 14168  df-clat 14230  df-oposet 29988  df-ol 29990  df-oml 29991  df-covers 30078  df-ats 30079  df-atl 30110  df-cvlat 30134  df-hlat 30163
  Copyright terms: Public domain W3C validator