Metamath Proof Explorer

Theorem cvrat4

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 analog.) (Contributed by NM, 30-Nov-2011)

Ref Expression
Hypotheses cvrat4.b 
|- B = ( Base ` K )
cvrat4.l 
|- .<_ = ( le ` K )
cvrat4.j 
|- .\/ = ( join ` K )
cvrat4.z 
|- .0. = ( 0. ` K )
cvrat4.a 
|- A = ( Atoms ` K )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 cvrat4.b 
 |-  B = ( Base ` K )
2 cvrat4.l 
 |-  .<_ = ( le ` K )
3 cvrat4.j 
 |-  .\/ = ( join ` K )
4 cvrat4.z 
 |-  .0. = ( 0. ` K )
5 cvrat4.a 
 |-  A = ( Atoms ` K )
6 hlatl 
 |-  ( K e. HL -> K e. AtLat )
7 6 adantr 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. AtLat )
8 simpr1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> X e. B )
9 1 2 4 5 atlex 
 |-  ( ( K e. AtLat /\ X e. B /\ X =/= .0. ) -> E. r e. A r .<_ X )
10 9 3exp 
 |-  ( K e. AtLat -> ( X e. B -> ( X =/= .0. -> E. r e. A r .<_ X ) ) )
11 7 8 10 sylc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X =/= .0. -> E. r e. A r .<_ X ) )
12 11 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P = Q ) -> ( X =/= .0. -> E. r e. A r .<_ X ) )
13 simpll 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ r e. A ) -> K e. HL )
14 simplr3 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ r e. A ) -> Q e. A )
15 simpr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ r e. A ) -> r e. A )
16 2 3 5 hlatlej1 
 |-  ( ( K e. HL /\ Q e. A /\ r e. A ) -> Q .<_ ( Q .\/ r ) )
17 13 14 15 16 syl3anc 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ r e. A ) -> Q .<_ ( Q .\/ r ) )
18 breq1 
 |-  ( P = Q -> ( P .<_ ( Q .\/ r ) <-> Q .<_ ( Q .\/ r ) ) )
19 17 18 syl5ibr 
 |-  ( P = Q -> ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ r e. A ) -> P .<_ ( Q .\/ r ) ) )
20 19 expd 
 |-  ( P = Q -> ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( r e. A -> P .<_ ( Q .\/ r ) ) ) )
21 20 impcom 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P = Q ) -> ( r e. A -> P .<_ ( Q .\/ r ) ) )
22 21 anim2d 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P = Q ) -> ( ( r .<_ X /\ r e. A ) -> ( r .<_ X /\ P .<_ ( Q .\/ r ) ) ) )
23 22 expcomd 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P = Q ) -> ( r e. A -> ( r .<_ X -> ( r .<_ X /\ P .<_ ( Q .\/ r ) ) ) ) )
24 23 reximdvai 
 |-  ( ( ( 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 ) ) ) )
25 12 24 syld 
 |-  ( ( ( 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 ) ) ) )
26 25 ex 
 |-  ( ( 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 ) ) ) ) )
27 26 a1i 
 |-  ( 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 ) ) ) ) ) )
28 27 com4l 
 |-  ( ( 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 ) ) ) ) ) )
29 28 imp4a 
 |-  ( ( 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 
 |-  ( K e. HL -> K e. Lat )
31 30 adantr 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. Lat )
32 simpr3 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q e. A )
33 1 5 atbase 
 |-  ( Q e. A -> Q e. B )
34 32 33 syl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q e. B )
35 1 2 3 latleeqj2 
 |-  ( ( K e. Lat /\ Q e. B /\ X e. B ) -> ( Q .<_ X <-> ( X .\/ Q ) = X ) )
36 31 34 8 35 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( Q .<_ X <-> ( X .\/ Q ) = X ) )
37 36 biimpa 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ Q .<_ X ) -> ( X .\/ Q ) = X )
38 37 breq2d 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ Q .<_ X ) -> ( P .<_ ( X .\/ Q ) <-> P .<_ X ) )
39 38 biimpa 
 |-  ( ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ Q .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> P .<_ X )
40 39 expl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( Q .<_ X /\ P .<_ ( X .\/ Q ) ) -> P .<_ X ) )
41 simpl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. HL )
42 simpr2 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> P e. A )
43 2 3 5 hlatlej2 
 |-  ( ( K e. HL /\ Q e. A /\ P e. A ) -> P .<_ ( Q .\/ P ) )
44 41 32 42 43 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> P .<_ ( Q .\/ P ) )
45 40 44 jctird 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( Q .<_ X /\ P .<_ ( X .\/ Q ) ) -> ( P .<_ X /\ P .<_ ( Q .\/ P ) ) ) )
46 45 42 jctild 
 |-  ( ( 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 ) ) ) ) )
47 46 impl 
 |-  ( ( ( ( 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 
 |-  ( r = P -> ( r .<_ X <-> P .<_ X ) )
49 oveq2 
 |-  ( r = P -> ( Q .\/ r ) = ( Q .\/ P ) )
50 49 breq2d 
 |-  ( r = P -> ( P .<_ ( Q .\/ r ) <-> P .<_ ( Q .\/ P ) ) )
51 48 50 anbi12d 
 |-  ( r = P -> ( ( r .<_ X /\ P .<_ ( Q .\/ r ) ) <-> ( P .<_ X /\ P .<_ ( Q .\/ P ) ) ) )
52 51 rspcev 
 |-  ( ( P e. A /\ ( P .<_ X /\ P .<_ ( Q .\/ P ) ) ) -> E. r e. A ( r .<_ X /\ P .<_ ( Q .\/ r ) ) )
53 47 52 syl 
 |-  ( ( ( ( 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 ) ) )
54 53 adantrl 
 |-  ( ( ( ( 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 ) ) )
55 54 exp31 
 |-  ( ( 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 
 |-  ( ( X =/= .0. /\ P .<_ ( X .\/ Q ) ) -> P .<_ ( X .\/ Q ) )
57 ioran 
 |-  ( -. ( P = Q \/ Q .<_ X ) <-> ( -. P = Q /\ -. Q .<_ X ) )
58 df-ne 
 |-  ( P =/= Q <-> -. P = Q )
59 58 anbi1i 
 |-  ( ( P =/= Q /\ -. Q .<_ X ) <-> ( -. P = Q /\ -. Q .<_ X ) )
60 57 59 bitr4i 
 |-  ( -. ( P = Q \/ Q .<_ X ) <-> ( P =/= Q /\ -. Q .<_ X ) )
61 eqid 
 |-  ( meet ` K ) = ( meet ` K )
62 1 2 3 61 5 cvrat3 
 |-  ( ( 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 ) )
63 62 3expd 
 |-  ( ( 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 ) ) ) )
64 63 imp4c 
 |-  ( ( 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 ) )
65 1 5 atbase 
 |-  ( P e. A -> P e. B )
66 42 65 syl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> P e. B )
67 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) e. B )
68 31 66 34 67 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( P .\/ Q ) e. B )
69 1 2 61 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ ( P .\/ Q ) e. B ) -> ( X ( meet ` K ) ( P .\/ Q ) ) .<_ X )
70 31 8 68 69 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X ( meet ` K ) ( P .\/ Q ) ) .<_ X )
71 70 adantr 
 |-  ( ( ( 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 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ ( ( P =/= Q /\ -. Q .<_ X ) /\ P .<_ ( X .\/ Q ) ) ) -> K e. HL )
73 63 imp44 
 |-  ( ( ( 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 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ ( ( P =/= Q /\ -. Q .<_ X ) /\ P .<_ ( X .\/ Q ) ) ) -> P e. A )
75 34 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ ( ( P =/= Q /\ -. Q .<_ X ) /\ P .<_ ( X .\/ Q ) ) ) -> Q e. B )
76 73 74 75 3jca 
 |-  ( ( ( 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 ) )
77 72 76 jca 
 |-  ( ( ( 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 ) ) )
78 1 2 61 4 5 atnle 
 |-  ( ( K e. AtLat /\ Q e. A /\ X e. B ) -> ( -. Q .<_ X <-> ( Q ( meet ` K ) X ) = .0. ) )
79 7 32 8 78 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( -. Q .<_ X <-> ( Q ( meet ` K ) X ) = .0. ) )
80 1 61 latmcom 
 |-  ( ( K e. Lat /\ Q e. B /\ X e. B ) -> ( Q ( meet ` K ) X ) = ( X ( meet ` K ) Q ) )
81 31 34 8 80 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( Q ( meet ` K ) X ) = ( X ( meet ` K ) Q ) )
82 81 eqeq1d 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( Q ( meet ` K ) X ) = .0. <-> ( X ( meet ` K ) Q ) = .0. ) )
83 79 82 bitrd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( -. Q .<_ X <-> ( X ( meet ` K ) Q ) = .0. ) )
84 1 61 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( P .\/ Q ) e. B ) -> ( X ( meet ` K ) ( P .\/ Q ) ) e. B )
85 31 8 68 84 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X ( meet ` K ) ( P .\/ Q ) ) e. B )
86 85 8 34 3jca 
 |-  ( ( 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 ) )
87 31 86 jca 
 |-  ( ( 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 ) ) )
88 1 2 61 latmlem2 
 |-  ( ( 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 ) ) )
89 87 70 88 sylc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( Q ( meet ` K ) ( X ( meet ` K ) ( P .\/ Q ) ) ) .<_ ( Q ( meet ` K ) X ) )
90 89 81 breqtrd 
 |-  ( ( 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 
 |-  ( ( 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. ) )
92 90 91 syl5ibcom 
 |-  ( ( 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 
 |-  ( K e. HL -> K e. OP )
94 93 adantr 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. OP )
95 1 61 latmcl 
 |-  ( ( K e. Lat /\ Q e. B /\ ( X ( meet ` K ) ( P .\/ Q ) ) e. B ) -> ( Q ( meet ` K ) ( X ( meet ` K ) ( P .\/ Q ) ) ) e. B )
96 31 34 85 95 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( Q ( meet ` K ) ( X ( meet ` K ) ( P .\/ Q ) ) ) e. B )
97 1 2 4 ople0 
 |-  ( ( 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. ) )
98 94 96 97 syl2anc 
 |-  ( ( 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. ) )
99 92 98 sylibd 
 |-  ( ( 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. ) )
100 83 99 sylbid 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( -. Q .<_ X -> ( Q ( meet ` K ) ( X ( meet ` K ) ( P .\/ Q ) ) ) = .0. ) )
101 100 imp 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ -. Q .<_ X ) -> ( Q ( meet ` K ) ( X ( meet ` K ) ( P .\/ Q ) ) ) = .0. )
102 101 adantrl 
 |-  ( ( ( 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. )
103 102 adantrr 
 |-  ( ( ( 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. )
104 1 2 61 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ ( P .\/ Q ) e. B ) -> ( X ( meet ` K ) ( P .\/ Q ) ) .<_ ( P .\/ Q ) )
105 31 8 68 104 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X ( meet ` K ) ( P .\/ Q ) ) .<_ ( P .\/ Q ) )
106 1 3 latjcom 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) = ( Q .\/ P ) )
107 31 66 34 106 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( P .\/ Q ) = ( Q .\/ P ) )
108 105 107 breqtrd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X ( meet ` K ) ( P .\/ Q ) ) .<_ ( Q .\/ P ) )
109 108 adantr 
 |-  ( ( ( 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 ) )
110 30 adantr 
 |-  ( ( K e. HL /\ ( ( X ( meet ` K ) ( P .\/ Q ) ) e. A /\ P e. A /\ Q e. B ) ) -> K e. Lat )
111 simpr3 
 |-  ( ( K e. HL /\ ( ( X ( meet ` K ) ( P .\/ Q ) ) e. A /\ P e. A /\ Q e. B ) ) -> Q e. B )
112 simpr1 
 |-  ( ( K e. HL /\ ( ( X ( meet ` K ) ( P .\/ Q ) ) e. A /\ P e. A /\ Q e. B ) ) -> ( X ( meet ` K ) ( P .\/ Q ) ) e. A )
113 1 5 atbase 
 |-  ( ( X ( meet ` K ) ( P .\/ Q ) ) e. A -> ( X ( meet ` K ) ( P .\/ Q ) ) e. B )
114 112 113 syl 
 |-  ( ( K e. HL /\ ( ( X ( meet ` K ) ( P .\/ Q ) ) e. A /\ P e. A /\ Q e. B ) ) -> ( X ( meet ` K ) ( P .\/ Q ) ) e. B )
115 1 61 latmcom 
 |-  ( ( 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 ) )
116 110 111 114 115 syl3anc 
 |-  ( ( 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 ) )
117 116 eqeq1d 
 |-  ( ( 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. ) )
118 1 2 3 61 4 5 hlexch3 
 |-  ( ( 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 ) ) ) ) )
119 118 3expia 
 |-  ( ( 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 ) ) ) ) ) )
120 117 119 sylbid 
 |-  ( ( 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 ) ) ) ) ) )
121 77 103 109 120 syl3c 
 |-  ( ( ( 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 ) ) ) )
122 71 121 jca 
 |-  ( ( ( 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 ) ) ) ) )
123 122 ex 
 |-  ( ( 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 ) ) ) ) ) )
124 64 123 jcad 
 |-  ( ( 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 
 |-  ( r = ( X ( meet ` K ) ( P .\/ Q ) ) -> ( r .<_ X <-> ( X ( meet ` K ) ( P .\/ Q ) ) .<_ X ) )
126 oveq2 
 |-  ( r = ( X ( meet ` K ) ( P .\/ Q ) ) -> ( Q .\/ r ) = ( Q .\/ ( X ( meet ` K ) ( P .\/ Q ) ) ) )
127 126 breq2d 
 |-  ( r = ( X ( meet ` K ) ( P .\/ Q ) ) -> ( P .<_ ( Q .\/ r ) <-> P .<_ ( Q .\/ ( X ( meet ` K ) ( P .\/ Q ) ) ) ) )
128 125 127 anbi12d 
 |-  ( r = ( X ( meet ` K ) ( P .\/ Q ) ) -> ( ( r .<_ X /\ P .<_ ( Q .\/ r ) ) <-> ( ( X ( meet ` K ) ( P .\/ Q ) ) .<_ X /\ P .<_ ( Q .\/ ( X ( meet ` K ) ( P .\/ Q ) ) ) ) ) )
129 128 rspcev 
 |-  ( ( ( 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 ) ) )
130 124 129 syl6 
 |-  ( ( 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 ) ) ) )
131 130 expd 
 |-  ( ( 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 ) ) ) ) )
132 60 131 syl5bi 
 |-  ( ( 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 ) ) ) ) )
133 56 132 syl7 
 |-  ( ( 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 ) ) ) ) )
134 29 55 133 ecase3d 
 |-  ( ( 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 ) ) ) )