This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvratlem

Description: Lemma for cvrat . ( atcvatlem analog.) (Contributed by NM, 22-Nov-2011)

Ref Expression
Hypotheses cvrat.b 
|- B = ( Base ` K )
cvrat.s 
|- .< = ( lt ` K )
cvrat.j 
|- .\/ = ( join ` K )
cvrat.z 
|- .0. = ( 0. ` K )
cvrat.a 
|- A = ( Atoms ` K )
Assertion cvratlem 
|- ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ ( X =/= .0. /\ X .< ( P .\/ Q ) ) ) -> ( -. P ( le ` K ) X -> X e. A ) )

Proof

Step Hyp Ref Expression
1 cvrat.b 
 |-  B = ( Base ` K )
2 cvrat.s 
 |-  .< = ( lt ` K )
3 cvrat.j 
 |-  .\/ = ( join ` K )
4 cvrat.z 
 |-  .0. = ( 0. ` K )
5 cvrat.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 eqid 
 |-  ( le ` K ) = ( le ` K )
10 1 9 4 5 atlex 
 |-  ( ( K e. AtLat /\ X e. B /\ X =/= .0. ) -> E. r e. A r ( le ` K ) X )
11 10 3expia 
 |-  ( ( K e. AtLat /\ X e. B ) -> ( X =/= .0. -> E. r e. A r ( le ` K ) X ) )
12 7 8 11 syl2anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X =/= .0. -> E. r e. A r ( le ` K ) X ) )
13 6 3ad2ant1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> K e. AtLat )
14 simp22 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> P e. A )
15 simp3 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> r e. A )
16 9 5 atcmp 
 |-  ( ( K e. AtLat /\ P e. A /\ r e. A ) -> ( P ( le ` K ) r <-> P = r ) )
17 13 14 15 16 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( P ( le ` K ) r <-> P = r ) )
18 breq1 
 |-  ( P = r -> ( P ( le ` K ) X <-> r ( le ` K ) X ) )
19 18 biimprd 
 |-  ( P = r -> ( r ( le ` K ) X -> P ( le ` K ) X ) )
20 17 19 biimtrdi 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( P ( le ` K ) r -> ( r ( le ` K ) X -> P ( le ` K ) X ) ) )
21 20 com23 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r ( le ` K ) X -> ( P ( le ` K ) r -> P ( le ` K ) X ) ) )
22 con3 
 |-  ( ( P ( le ` K ) r -> P ( le ` K ) X ) -> ( -. P ( le ` K ) X -> -. P ( le ` K ) r ) )
23 21 22 syl6 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r ( le ` K ) X -> ( -. P ( le ` K ) X -> -. P ( le ` K ) r ) ) )
24 23 impd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( ( r ( le ` K ) X /\ -. P ( le ` K ) X ) -> -. P ( le ` K ) r ) )
25 simp1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> K e. HL )
26 1 5 atbase 
 |-  ( r e. A -> r e. B )
27 26 3ad2ant3 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> r e. B )
28 eqid 
 |-  (
29 1 9 3 28 5 cvr1 
 |-  ( ( K e. HL /\ r e. B /\ P e. A ) -> ( -. P ( le ` K ) r <-> r (
30 25 27 14 29 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( -. P ( le ` K ) r <-> r (
31 24 30 sylibd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( ( r ( le ` K ) X /\ -. P ( le ` K ) X ) -> r (
32 31 imp 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ -. P ( le ` K ) X ) ) -> r (
33 hllat 
 |-  ( K e. HL -> K e. Lat )
34 33 3ad2ant1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> K e. Lat )
35 1 5 atbase 
 |-  ( P e. A -> P e. B )
36 14 35 syl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> P e. B )
37 1 3 latjcom 
 |-  ( ( K e. Lat /\ P e. B /\ r e. B ) -> ( P .\/ r ) = ( r .\/ P ) )
38 34 36 27 37 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( P .\/ r ) = ( r .\/ P ) )
39 38 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ -. P ( le ` K ) X ) ) -> ( P .\/ r ) = ( r .\/ P ) )
40 32 39 breqtrrd 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ -. P ( le ` K ) X ) ) -> r (
41 40 adantrrl 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> r (
42 9 3 5 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ r e. A ) -> P ( le ` K ) ( P .\/ r ) )
43 25 14 15 42 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> P ( le ` K ) ( P .\/ r ) )
44 43 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> P ( le ` K ) ( P .\/ r ) )
45 9 5 atcmp 
 |-  ( ( K e. AtLat /\ r e. A /\ P e. A ) -> ( r ( le ` K ) P <-> r = P ) )
46 13 15 14 45 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r ( le ` K ) P <-> r = P ) )
47 breq1 
 |-  ( r = P -> ( r ( le ` K ) X <-> P ( le ` K ) X ) )
48 47 biimpd 
 |-  ( r = P -> ( r ( le ` K ) X -> P ( le ` K ) X ) )
49 46 48 biimtrdi 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r ( le ` K ) P -> ( r ( le ` K ) X -> P ( le ` K ) X ) ) )
50 49 com23 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r ( le ` K ) X -> ( r ( le ` K ) P -> P ( le ` K ) X ) ) )
51 con3 
 |-  ( ( r ( le ` K ) P -> P ( le ` K ) X ) -> ( -. P ( le ` K ) X -> -. r ( le ` K ) P ) )
52 50 51 syl6 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r ( le ` K ) X -> ( -. P ( le ` K ) X -> -. r ( le ` K ) P ) ) )
53 52 imp32 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ -. P ( le ` K ) X ) ) -> -. r ( le ` K ) P )
54 53 adantrrl 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> -. r ( le ` K ) P )
55 simprl 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ X .< ( P .\/ Q ) ) ) -> r ( le ` K ) X )
56 simp21 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> X e. B )
57 simp23 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> Q e. A )
58 1 5 atbase 
 |-  ( Q e. A -> Q e. B )
59 57 58 syl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> Q e. B )
60 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) e. B )
61 34 36 59 60 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( P .\/ Q ) e. B )
62 25 56 61 3jca 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( K e. HL /\ X e. B /\ ( P .\/ Q ) e. B ) )
63 9 2 pltle 
 |-  ( ( K e. HL /\ X e. B /\ ( P .\/ Q ) e. B ) -> ( X .< ( P .\/ Q ) -> X ( le ` K ) ( P .\/ Q ) ) )
64 63 imp 
 |-  ( ( ( K e. HL /\ X e. B /\ ( P .\/ Q ) e. B ) /\ X .< ( P .\/ Q ) ) -> X ( le ` K ) ( P .\/ Q ) )
65 62 64 sylan 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ X .< ( P .\/ Q ) ) -> X ( le ` K ) ( P .\/ Q ) )
66 65 adantrl 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ X .< ( P .\/ Q ) ) ) -> X ( le ` K ) ( P .\/ Q ) )
67 hlpos 
 |-  ( K e. HL -> K e. Poset )
68 67 3ad2ant1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> K e. Poset )
69 1 9 postr 
 |-  ( ( K e. Poset /\ ( r e. B /\ X e. B /\ ( P .\/ Q ) e. B ) ) -> ( ( r ( le ` K ) X /\ X ( le ` K ) ( P .\/ Q ) ) -> r ( le ` K ) ( P .\/ Q ) ) )
70 68 27 56 61 69 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( ( r ( le ` K ) X /\ X ( le ` K ) ( P .\/ Q ) ) -> r ( le ` K ) ( P .\/ Q ) ) )
71 70 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ X .< ( P .\/ Q ) ) ) -> ( ( r ( le ` K ) X /\ X ( le ` K ) ( P .\/ Q ) ) -> r ( le ` K ) ( P .\/ Q ) ) )
72 55 66 71 mp2and 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ X .< ( P .\/ Q ) ) ) -> r ( le ` K ) ( P .\/ Q ) )
73 72 adantrrr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> r ( le ` K ) ( P .\/ Q ) )
74 1 9 3 5 hlexch1 
 |-  ( ( K e. HL /\ ( r e. A /\ Q e. A /\ P e. B ) /\ -. r ( le ` K ) P ) -> ( r ( le ` K ) ( P .\/ Q ) -> Q ( le ` K ) ( P .\/ r ) ) )
75 74 3expia 
 |-  ( ( K e. HL /\ ( r e. A /\ Q e. A /\ P e. B ) ) -> ( -. r ( le ` K ) P -> ( r ( le ` K ) ( P .\/ Q ) -> Q ( le ` K ) ( P .\/ r ) ) ) )
76 75 impd 
 |-  ( ( K e. HL /\ ( r e. A /\ Q e. A /\ P e. B ) ) -> ( ( -. r ( le ` K ) P /\ r ( le ` K ) ( P .\/ Q ) ) -> Q ( le ` K ) ( P .\/ r ) ) )
77 25 15 57 36 76 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( ( -. r ( le ` K ) P /\ r ( le ` K ) ( P .\/ Q ) ) -> Q ( le ` K ) ( P .\/ r ) ) )
78 77 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( ( -. r ( le ` K ) P /\ r ( le ` K ) ( P .\/ Q ) ) -> Q ( le ` K ) ( P .\/ r ) ) )
79 54 73 78 mp2and 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> Q ( le ` K ) ( P .\/ r ) )
80 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ r e. B ) -> ( P .\/ r ) e. B )
81 34 36 27 80 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( P .\/ r ) e. B )
82 1 9 3 latjle12 
 |-  ( ( K e. Lat /\ ( P e. B /\ Q e. B /\ ( P .\/ r ) e. B ) ) -> ( ( P ( le ` K ) ( P .\/ r ) /\ Q ( le ` K ) ( P .\/ r ) ) <-> ( P .\/ Q ) ( le ` K ) ( P .\/ r ) ) )
83 34 36 59 81 82 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( ( P ( le ` K ) ( P .\/ r ) /\ Q ( le ` K ) ( P .\/ r ) ) <-> ( P .\/ Q ) ( le ` K ) ( P .\/ r ) ) )
84 83 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( ( P ( le ` K ) ( P .\/ r ) /\ Q ( le ` K ) ( P .\/ r ) ) <-> ( P .\/ Q ) ( le ` K ) ( P .\/ r ) ) )
85 44 79 84 mpbi2and 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( P .\/ Q ) ( le ` K ) ( P .\/ r ) )
86 9 3 5 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> P ( le ` K ) ( P .\/ Q ) )
87 25 14 57 86 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> P ( le ` K ) ( P .\/ Q ) )
88 87 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> P ( le ` K ) ( P .\/ Q ) )
89 1 9 3 latjle12 
 |-  ( ( K e. Lat /\ ( P e. B /\ r e. B /\ ( P .\/ Q ) e. B ) ) -> ( ( P ( le ` K ) ( P .\/ Q ) /\ r ( le ` K ) ( P .\/ Q ) ) <-> ( P .\/ r ) ( le ` K ) ( P .\/ Q ) ) )
90 34 36 27 61 89 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( ( P ( le ` K ) ( P .\/ Q ) /\ r ( le ` K ) ( P .\/ Q ) ) <-> ( P .\/ r ) ( le ` K ) ( P .\/ Q ) ) )
91 90 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( ( P ( le ` K ) ( P .\/ Q ) /\ r ( le ` K ) ( P .\/ Q ) ) <-> ( P .\/ r ) ( le ` K ) ( P .\/ Q ) ) )
92 88 73 91 mpbi2and 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( P .\/ r ) ( le ` K ) ( P .\/ Q ) )
93 34 61 81 3jca 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( K e. Lat /\ ( P .\/ Q ) e. B /\ ( P .\/ r ) e. B ) )
94 93 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( K e. Lat /\ ( P .\/ Q ) e. B /\ ( P .\/ r ) e. B ) )
95 1 9 latasymb 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. B /\ ( P .\/ r ) e. B ) -> ( ( ( P .\/ Q ) ( le ` K ) ( P .\/ r ) /\ ( P .\/ r ) ( le ` K ) ( P .\/ Q ) ) <-> ( P .\/ Q ) = ( P .\/ r ) ) )
96 94 95 syl 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( ( ( P .\/ Q ) ( le ` K ) ( P .\/ r ) /\ ( P .\/ r ) ( le ` K ) ( P .\/ Q ) ) <-> ( P .\/ Q ) = ( P .\/ r ) ) )
97 85 92 96 mpbi2and 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( P .\/ Q ) = ( P .\/ r ) )
98 breq2 
 |-  ( ( P .\/ Q ) = ( P .\/ r ) -> ( X .< ( P .\/ Q ) <-> X .< ( P .\/ r ) ) )
99 98 biimpcd 
 |-  ( X .< ( P .\/ Q ) -> ( ( P .\/ Q ) = ( P .\/ r ) -> X .< ( P .\/ r ) ) )
100 99 adantr 
 |-  ( ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) -> ( ( P .\/ Q ) = ( P .\/ r ) -> X .< ( P .\/ r ) ) )
101 100 ad2antll 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( ( P .\/ Q ) = ( P .\/ r ) -> X .< ( P .\/ r ) ) )
102 97 101 mpd 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> X .< ( P .\/ r ) )
103 1 9 2 28 cvrnbtwn3 
 |-  ( ( K e. Poset /\ ( r e. B /\ ( P .\/ r ) e. B /\ X e. B ) /\ r (  ( ( r ( le ` K ) X /\ X .< ( P .\/ r ) ) <-> r = X ) )
104 103 biimpd 
 |-  ( ( K e. Poset /\ ( r e. B /\ ( P .\/ r ) e. B /\ X e. B ) /\ r (  ( ( r ( le ` K ) X /\ X .< ( P .\/ r ) ) -> r = X ) )
105 104 3expia 
 |-  ( ( K e. Poset /\ ( r e. B /\ ( P .\/ r ) e. B /\ X e. B ) ) -> ( r (  ( ( r ( le ` K ) X /\ X .< ( P .\/ r ) ) -> r = X ) ) )
106 68 27 81 56 105 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r (  ( ( r ( le ` K ) X /\ X .< ( P .\/ r ) ) -> r = X ) ) )
107 106 exp4a 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r (  ( r ( le ` K ) X -> ( X .< ( P .\/ r ) -> r = X ) ) ) )
108 107 com23 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r ( le ` K ) X -> ( r (  ( X .< ( P .\/ r ) -> r = X ) ) ) )
109 108 imp4b 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ r ( le ` K ) X ) -> ( ( r (  r = X ) )
110 109 adantrr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> ( ( r (  r = X ) )
111 41 102 110 mp2and 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> r = X )
112 simpl3 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> r e. A )
113 111 112 eqeltrrd 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) /\ ( r ( le ` K ) X /\ ( X .< ( P .\/ Q ) /\ -. P ( le ` K ) X ) ) ) -> X e. A )
114 113 exp45 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) /\ r e. A ) -> ( r ( le ` K ) X -> ( X .< ( P .\/ Q ) -> ( -. P ( le ` K ) X -> X e. A ) ) ) )
115 114 3expa 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ r e. A ) -> ( r ( le ` K ) X -> ( X .< ( P .\/ Q ) -> ( -. P ( le ` K ) X -> X e. A ) ) ) )
116 115 rexlimdva 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( E. r e. A r ( le ` K ) X -> ( X .< ( P .\/ Q ) -> ( -. P ( le ` K ) X -> X e. A ) ) ) )
117 12 116 syld 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X =/= .0. -> ( X .< ( P .\/ Q ) -> ( -. P ( le ` K ) X -> X e. A ) ) ) )
118 117 imp32 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ ( X =/= .0. /\ X .< ( P .\/ Q ) ) ) -> ( -. P ( le ` K ) X -> X e. A ) )