Metamath Proof Explorer

Theorem cdlemblem

Description: Lemma for cdlemb . (Contributed by NM, 8-May-2012)

Ref Expression
Hypotheses cdlemb.b 
|- B = ( Base ` K )
cdlemb.l 
|- .<_ = ( le ` K )
cdlemb.j 
|- .\/ = ( join ` K )
cdlemb.u 
|- .1. = ( 1. ` K )
cdlemb.c 
|- C = (
cdlemb.a 
|- A = ( Atoms ` K )
cdlemblem.s 
|- .< = ( lt ` K )
cdlemblem.m 
|- ./\ = ( meet ` K )
cdlemblem.v 
|- V = ( ( P .\/ Q ) ./\ X )
Assertion cdlemblem 
|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) )

Proof

Step Hyp Ref Expression
1 cdlemb.b 
 |-  B = ( Base ` K )
2 cdlemb.l 
 |-  .<_ = ( le ` K )
3 cdlemb.j 
 |-  .\/ = ( join ` K )
4 cdlemb.u 
 |-  .1. = ( 1. ` K )
5 cdlemb.c 
 |-  C = (
6 cdlemb.a 
 |-  A = ( Atoms ` K )
7 cdlemblem.s 
 |-  .< = ( lt ` K )
8 cdlemblem.m 
 |-  ./\ = ( meet ` K )
9 cdlemblem.v 
 |-  V = ( ( P .\/ Q ) ./\ X )
10 simp132 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> -. P .<_ X )
11 simp111 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> K e. HL )
12 simp2l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> u e. A )
13 simp12l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> X e. B )
14 11 12 13 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( K e. HL /\ u e. A /\ X e. B ) )
15 simp2rr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> u .< X )
16 2 7 pltle 
 |-  ( ( K e. HL /\ u e. A /\ X e. B ) -> ( u .< X -> u .<_ X ) )
17 14 15 16 sylc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> u .<_ X )
18 11 hllatd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> K e. Lat )
19 simp3l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> r e. A )
20 1 6 atbase 
 |-  ( r e. A -> r e. B )
21 19 20 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> r e. B )
22 1 6 atbase 
 |-  ( u e. A -> u e. B )
23 12 22 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> u e. B )
24 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( r e. B /\ u e. B /\ X e. B ) ) -> ( ( r .<_ X /\ u .<_ X ) <-> ( r .\/ u ) .<_ X ) )
25 18 21 23 13 24 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( ( r .<_ X /\ u .<_ X ) <-> ( r .\/ u ) .<_ X ) )
26 25 biimpd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( ( r .<_ X /\ u .<_ X ) -> ( r .\/ u ) .<_ X ) )
27 17 26 mpan2d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r .<_ X -> ( r .\/ u ) .<_ X ) )
28 simp112 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> P e. A )
29 19 28 12 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r e. A /\ P e. A /\ u e. A ) )
30 simp3r2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> r =/= u )
31 11 29 30 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( K e. HL /\ ( r e. A /\ P e. A /\ u e. A ) /\ r =/= u ) )
32 simp3r3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> r .<_ ( P .\/ u ) )
33 2 3 6 hlatexch2 
 |-  ( ( K e. HL /\ ( r e. A /\ P e. A /\ u e. A ) /\ r =/= u ) -> ( r .<_ ( P .\/ u ) -> P .<_ ( r .\/ u ) ) )
34 31 32 33 sylc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> P .<_ ( r .\/ u ) )
35 1 6 atbase 
 |-  ( P e. A -> P e. B )
36 28 35 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> P e. B )
37 1 3 latjcl 
 |-  ( ( K e. Lat /\ r e. B /\ u e. B ) -> ( r .\/ u ) e. B )
38 18 21 23 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r .\/ u ) e. B )
39 1 2 lattr 
 |-  ( ( K e. Lat /\ ( P e. B /\ ( r .\/ u ) e. B /\ X e. B ) ) -> ( ( P .<_ ( r .\/ u ) /\ ( r .\/ u ) .<_ X ) -> P .<_ X ) )
40 18 36 38 13 39 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( ( P .<_ ( r .\/ u ) /\ ( r .\/ u ) .<_ X ) -> P .<_ X ) )
41 34 40 mpand 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( ( r .\/ u ) .<_ X -> P .<_ X ) )
42 27 41 syld 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r .<_ X -> P .<_ X ) )
43 10 42 mtod 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> -. r .<_ X )
44 simp2rl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> u =/= V )
45 simp113 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> Q e. A )
46 simp3r1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> r =/= P )
47 2 3 6 hlatexchb1 
 |-  ( ( K e. HL /\ ( r e. A /\ Q e. A /\ P e. A ) /\ r =/= P ) -> ( r .<_ ( P .\/ Q ) <-> ( P .\/ r ) = ( P .\/ Q ) ) )
48 11 19 45 28 46 47 syl131anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r .<_ ( P .\/ Q ) <-> ( P .\/ r ) = ( P .\/ Q ) ) )
49 19 12 28 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r e. A /\ u e. A /\ P e. A ) )
50 11 49 46 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( K e. HL /\ ( r e. A /\ u e. A /\ P e. A ) /\ r =/= P ) )
51 2 3 6 hlatexch1 
 |-  ( ( K e. HL /\ ( r e. A /\ u e. A /\ P e. A ) /\ r =/= P ) -> ( r .<_ ( P .\/ u ) -> u .<_ ( P .\/ r ) ) )
52 50 32 51 sylc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> u .<_ ( P .\/ r ) )
53 breq2 
 |-  ( ( P .\/ r ) = ( P .\/ Q ) -> ( u .<_ ( P .\/ r ) <-> u .<_ ( P .\/ Q ) ) )
54 52 53 syl5ibcom 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( ( P .\/ r ) = ( P .\/ Q ) -> u .<_ ( P .\/ Q ) ) )
55 48 54 sylbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r .<_ ( P .\/ Q ) -> u .<_ ( P .\/ Q ) ) )
56 55 17 jctird 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r .<_ ( P .\/ Q ) -> ( u .<_ ( P .\/ Q ) /\ u .<_ X ) ) )
57 1 6 atbase 
 |-  ( Q e. A -> Q e. B )
58 45 57 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> Q e. B )
59 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) e. B )
60 18 36 58 59 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( P .\/ Q ) e. B )
61 1 2 8 latlem12 
 |-  ( ( K e. Lat /\ ( u e. B /\ ( P .\/ Q ) e. B /\ X e. B ) ) -> ( ( u .<_ ( P .\/ Q ) /\ u .<_ X ) <-> u .<_ ( ( P .\/ Q ) ./\ X ) ) )
62 18 23 60 13 61 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( ( u .<_ ( P .\/ Q ) /\ u .<_ X ) <-> u .<_ ( ( P .\/ Q ) ./\ X ) ) )
63 9 breq2i 
 |-  ( u .<_ V <-> u .<_ ( ( P .\/ Q ) ./\ X ) )
64 62 63 bitr4di 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( ( u .<_ ( P .\/ Q ) /\ u .<_ X ) <-> u .<_ V ) )
65 56 64 sylibd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r .<_ ( P .\/ Q ) -> u .<_ V ) )
66 hlatl 
 |-  ( K e. HL -> K e. AtLat )
67 11 66 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> K e. AtLat )
68 simp12r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> P =/= Q )
69 simp131 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> X C .1. )
70 1 2 3 8 4 5 6 1cvrat 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P =/= Q /\ X C .1. /\ -. P .<_ X ) ) -> ( ( P .\/ Q ) ./\ X ) e. A )
71 11 28 45 13 68 69 10 70 syl133anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( ( P .\/ Q ) ./\ X ) e. A )
72 9 71 eqeltrid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> V e. A )
73 2 6 atcmp 
 |-  ( ( K e. AtLat /\ u e. A /\ V e. A ) -> ( u .<_ V <-> u = V ) )
74 67 12 72 73 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( u .<_ V <-> u = V ) )
75 65 74 sylibd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( r .<_ ( P .\/ Q ) -> u = V ) )
76 75 necon3ad 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( u =/= V -> -. r .<_ ( P .\/ Q ) ) )
77 44 76 mpd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> -. r .<_ ( P .\/ Q ) )
78 43 77 jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= V /\ u .< X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) )