Metamath Proof Explorer

Theorem 3dim2

Description: Construct 2 new layers on top of 2 given atoms. (Contributed by NM, 27-Jul-2012)

Ref Expression
Hypotheses 3dim0.j 
|- .\/ = ( join ` K )
3dim0.l 
|- .<_ = ( le ` K )
3dim0.a 
|- A = ( Atoms ` K )
Assertion 3dim2 
|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )

Proof

Step Hyp Ref Expression
1 3dim0.j 
 |-  .\/ = ( join ` K )
2 3dim0.l 
 |-  .<_ = ( le ` K )
3 3dim0.a 
 |-  A = ( Atoms ` K )
4 1 2 3 3dim1 
 |-  ( ( K e. HL /\ Q e. A ) -> E. u e. A E. v e. A E. w e. A ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) )
5 4 3adant2 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> E. u e. A E. v e. A E. w e. A ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) )
6 simpl21 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> u e. A )
7 simpl22 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> v e. A )
8 simp31 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> Q =/= u )
9 8 necomd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> u =/= Q )
10 9 adantr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> u =/= Q )
11 oveq1 
 |-  ( P = Q -> ( P .\/ Q ) = ( Q .\/ Q ) )
12 simp11 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> K e. HL )
13 simp13 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> Q e. A )
14 1 3 hlatjidm 
 |-  ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
15 12 13 14 syl2anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( Q .\/ Q ) = Q )
16 11 15 sylan9eqr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> ( P .\/ Q ) = Q )
17 16 breq2d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> ( u .<_ ( P .\/ Q ) <-> u .<_ Q ) )
18 17 notbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> ( -. u .<_ ( P .\/ Q ) <-> -. u .<_ Q ) )
19 hlatl 
 |-  ( K e. HL -> K e. AtLat )
20 12 19 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> K e. AtLat )
21 simp21 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> u e. A )
22 2 3 atncmp 
 |-  ( ( K e. AtLat /\ u e. A /\ Q e. A ) -> ( -. u .<_ Q <-> u =/= Q ) )
23 20 21 13 22 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( -. u .<_ Q <-> u =/= Q ) )
24 23 adantr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> ( -. u .<_ Q <-> u =/= Q ) )
25 18 24 bitrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> ( -. u .<_ ( P .\/ Q ) <-> u =/= Q ) )
26 10 25 mpbird 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> -. u .<_ ( P .\/ Q ) )
27 simpl32 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> -. v .<_ ( Q .\/ u ) )
28 16 oveq1d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> ( ( P .\/ Q ) .\/ u ) = ( Q .\/ u ) )
29 28 breq2d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> ( v .<_ ( ( P .\/ Q ) .\/ u ) <-> v .<_ ( Q .\/ u ) ) )
30 27 29 mtbird 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> -. v .<_ ( ( P .\/ Q ) .\/ u ) )
31 breq1 
 |-  ( r = u -> ( r .<_ ( P .\/ Q ) <-> u .<_ ( P .\/ Q ) ) )
32 31 notbid 
 |-  ( r = u -> ( -. r .<_ ( P .\/ Q ) <-> -. u .<_ ( P .\/ Q ) ) )
33 oveq2 
 |-  ( r = u -> ( ( P .\/ Q ) .\/ r ) = ( ( P .\/ Q ) .\/ u ) )
34 33 breq2d 
 |-  ( r = u -> ( s .<_ ( ( P .\/ Q ) .\/ r ) <-> s .<_ ( ( P .\/ Q ) .\/ u ) ) )
35 34 notbid 
 |-  ( r = u -> ( -. s .<_ ( ( P .\/ Q ) .\/ r ) <-> -. s .<_ ( ( P .\/ Q ) .\/ u ) ) )
36 32 35 anbi12d 
 |-  ( r = u -> ( ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) <-> ( -. u .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ u ) ) ) )
37 breq1 
 |-  ( s = v -> ( s .<_ ( ( P .\/ Q ) .\/ u ) <-> v .<_ ( ( P .\/ Q ) .\/ u ) ) )
38 37 notbid 
 |-  ( s = v -> ( -. s .<_ ( ( P .\/ Q ) .\/ u ) <-> -. v .<_ ( ( P .\/ Q ) .\/ u ) ) )
39 38 anbi2d 
 |-  ( s = v -> ( ( -. u .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ u ) ) <-> ( -. u .<_ ( P .\/ Q ) /\ -. v .<_ ( ( P .\/ Q ) .\/ u ) ) ) )
40 36 39 rspc2ev 
 |-  ( ( u e. A /\ v e. A /\ ( -. u .<_ ( P .\/ Q ) /\ -. v .<_ ( ( P .\/ Q ) .\/ u ) ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
41 6 7 26 30 40 syl112anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P = Q ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
42 simp22 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> v e. A )
43 simp23 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> w e. A )
44 42 43 jca 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( v e. A /\ w e. A ) )
45 44 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ u ) ) -> ( v e. A /\ w e. A ) )
46 simpll1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ u ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
47 simp32 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> -. v .<_ ( Q .\/ u ) )
48 simp33 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> -. w .<_ ( ( Q .\/ u ) .\/ v ) )
49 21 47 48 3jca 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( u e. A /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) )
50 49 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ u ) ) -> ( u e. A /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) )
51 simplr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ u ) ) -> P =/= Q )
52 simpr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ u ) ) -> P .<_ ( Q .\/ u ) )
53 1 2 3 3dimlem2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) /\ ( P =/= Q /\ P .<_ ( Q .\/ u ) ) ) -> ( P =/= Q /\ -. v .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ v ) ) )
54 46 50 51 52 53 syl112anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ u ) ) -> ( P =/= Q /\ -. v .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ v ) ) )
55 3simpc 
 |-  ( ( P =/= Q /\ -. v .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ v ) ) -> ( -. v .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ v ) ) )
56 54 55 syl 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ u ) ) -> ( -. v .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ v ) ) )
57 breq1 
 |-  ( r = v -> ( r .<_ ( P .\/ Q ) <-> v .<_ ( P .\/ Q ) ) )
58 57 notbid 
 |-  ( r = v -> ( -. r .<_ ( P .\/ Q ) <-> -. v .<_ ( P .\/ Q ) ) )
59 oveq2 
 |-  ( r = v -> ( ( P .\/ Q ) .\/ r ) = ( ( P .\/ Q ) .\/ v ) )
60 59 breq2d 
 |-  ( r = v -> ( s .<_ ( ( P .\/ Q ) .\/ r ) <-> s .<_ ( ( P .\/ Q ) .\/ v ) ) )
61 60 notbid 
 |-  ( r = v -> ( -. s .<_ ( ( P .\/ Q ) .\/ r ) <-> -. s .<_ ( ( P .\/ Q ) .\/ v ) ) )
62 58 61 anbi12d 
 |-  ( r = v -> ( ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) <-> ( -. v .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ v ) ) ) )
63 breq1 
 |-  ( s = w -> ( s .<_ ( ( P .\/ Q ) .\/ v ) <-> w .<_ ( ( P .\/ Q ) .\/ v ) ) )
64 63 notbid 
 |-  ( s = w -> ( -. s .<_ ( ( P .\/ Q ) .\/ v ) <-> -. w .<_ ( ( P .\/ Q ) .\/ v ) ) )
65 64 anbi2d 
 |-  ( s = w -> ( ( -. v .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ v ) ) <-> ( -. v .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ v ) ) ) )
66 62 65 rspc2ev 
 |-  ( ( v e. A /\ w e. A /\ ( -. v .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ v ) ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
67 66 3expa 
 |-  ( ( ( v e. A /\ w e. A ) /\ ( -. v .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ v ) ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
68 45 56 67 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ u ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
69 21 43 jca 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( u e. A /\ w e. A ) )
70 69 ad3antrrr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( u e. A /\ w e. A ) )
71 simp1 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
72 21 42 jca 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( u e. A /\ v e. A ) )
73 8 48 jca 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( Q =/= u /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) )
74 71 72 73 3jca 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A ) /\ ( Q =/= u /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) )
75 74 ad3antrrr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A ) /\ ( Q =/= u /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) )
76 simpllr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) -> P =/= Q )
77 simplr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) -> -. P .<_ ( Q .\/ u ) )
78 simpr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) -> P .<_ ( ( Q .\/ u ) .\/ v ) )
79 1 2 3 3dimlem3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A ) /\ ( Q =/= u /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ u ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( P =/= Q /\ -. u .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ u ) ) )
80 75 76 77 78 79 syl13anc 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( P =/= Q /\ -. u .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ u ) ) )
81 3simpc 
 |-  ( ( P =/= Q /\ -. u .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ u ) ) -> ( -. u .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ u ) ) )
82 80 81 syl 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( -. u .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ u ) ) )
83 breq1 
 |-  ( s = w -> ( s .<_ ( ( P .\/ Q ) .\/ u ) <-> w .<_ ( ( P .\/ Q ) .\/ u ) ) )
84 83 notbid 
 |-  ( s = w -> ( -. s .<_ ( ( P .\/ Q ) .\/ u ) <-> -. w .<_ ( ( P .\/ Q ) .\/ u ) ) )
85 84 anbi2d 
 |-  ( s = w -> ( ( -. u .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ u ) ) <-> ( -. u .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ u ) ) ) )
86 36 85 rspc2ev 
 |-  ( ( u e. A /\ w e. A /\ ( -. u .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ u ) ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
87 86 3expa 
 |-  ( ( ( u e. A /\ w e. A ) /\ ( -. u .<_ ( P .\/ Q ) /\ -. w .<_ ( ( P .\/ Q ) .\/ u ) ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
88 70 82 87 syl2anc 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ P .<_ ( ( Q .\/ u ) .\/ v ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
89 72 ad3antrrr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( u e. A /\ v e. A ) )
90 8 47 jca 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( Q =/= u /\ -. v .<_ ( Q .\/ u ) ) )
91 71 72 90 3jca 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) ) ) )
92 91 ad3antrrr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) ) ) )
93 simpllr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> P =/= Q )
94 simplr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> -. P .<_ ( Q .\/ u ) )
95 simpr 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> -. P .<_ ( ( Q .\/ u ) .\/ v ) )
96 1 2 3 3dimlem4 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( P =/= Q /\ -. u .<_ ( P .\/ Q ) /\ -. v .<_ ( ( P .\/ Q ) .\/ u ) ) )
97 92 93 94 95 96 syl121anc 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( P =/= Q /\ -. u .<_ ( P .\/ Q ) /\ -. v .<_ ( ( P .\/ Q ) .\/ u ) ) )
98 3simpc 
 |-  ( ( P =/= Q /\ -. u .<_ ( P .\/ Q ) /\ -. v .<_ ( ( P .\/ Q ) .\/ u ) ) -> ( -. u .<_ ( P .\/ Q ) /\ -. v .<_ ( ( P .\/ Q ) .\/ u ) ) )
99 97 98 syl 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> ( -. u .<_ ( P .\/ Q ) /\ -. v .<_ ( ( P .\/ Q ) .\/ u ) ) )
100 40 3expa 
 |-  ( ( ( u e. A /\ v e. A ) /\ ( -. u .<_ ( P .\/ Q ) /\ -. v .<_ ( ( P .\/ Q ) .\/ u ) ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
101 89 99 100 syl2anc 
 |-  ( ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) /\ -. P .<_ ( ( Q .\/ u ) .\/ v ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
102 88 101 pm2.61dan 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ u ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
103 68 102 pm2.61dan 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) /\ P =/= Q ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
104 41 103 pm2.61dane 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
105 104 3exp 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( u e. A /\ v e. A /\ w e. A ) -> ( ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) ) )
106 105 3expd 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( u e. A -> ( v e. A -> ( w e. A -> ( ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) ) ) ) )
107 106 imp32 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A ) ) -> ( w e. A -> ( ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) ) )
108 107 rexlimdv 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( u e. A /\ v e. A ) ) -> ( E. w e. A ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) )
109 108 rexlimdvva 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( E. u e. A E. v e. A E. w e. A ( Q =/= u /\ -. v .<_ ( Q .\/ u ) /\ -. w .<_ ( ( Q .\/ u ) .\/ v ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) )
110 5 109 mpd 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )