Metamath Proof Explorer

Theorem 3dim3

Description: Construct a new layer on top of 3 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 3dim3 
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> E. s e. A -. 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 3dim2 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> E. v e. A E. w e. A ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) )
5 4 3adant3r1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> E. v e. A E. w e. A ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) )
6 simpl2l 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P = Q ) -> v e. A )
7 simp3l 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> -. v .<_ ( Q .\/ R ) )
8 simp1l 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> K e. HL )
9 simp1r2 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> Q e. A )
10 1 3 hlatjidm 
 |-  ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
11 8 9 10 syl2anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> ( Q .\/ Q ) = Q )
12 11 oveq1d 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> ( ( Q .\/ Q ) .\/ R ) = ( Q .\/ R ) )
13 12 breq2d 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> ( v .<_ ( ( Q .\/ Q ) .\/ R ) <-> v .<_ ( Q .\/ R ) ) )
14 7 13 mtbird 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> -. v .<_ ( ( Q .\/ Q ) .\/ R ) )
15 oveq1 
 |-  ( P = Q -> ( P .\/ Q ) = ( Q .\/ Q ) )
16 15 oveq1d 
 |-  ( P = Q -> ( ( P .\/ Q ) .\/ R ) = ( ( Q .\/ Q ) .\/ R ) )
17 16 breq2d 
 |-  ( P = Q -> ( v .<_ ( ( P .\/ Q ) .\/ R ) <-> v .<_ ( ( Q .\/ Q ) .\/ R ) ) )
18 17 notbid 
 |-  ( P = Q -> ( -. v .<_ ( ( P .\/ Q ) .\/ R ) <-> -. v .<_ ( ( Q .\/ Q ) .\/ R ) ) )
19 18 biimparc 
 |-  ( ( -. v .<_ ( ( Q .\/ Q ) .\/ R ) /\ P = Q ) -> -. v .<_ ( ( P .\/ Q ) .\/ R ) )
20 14 19 sylan 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P = Q ) -> -. v .<_ ( ( P .\/ Q ) .\/ R ) )
21 breq1 
 |-  ( s = v -> ( s .<_ ( ( P .\/ Q ) .\/ R ) <-> v .<_ ( ( P .\/ Q ) .\/ R ) ) )
22 21 notbid 
 |-  ( s = v -> ( -. s .<_ ( ( P .\/ Q ) .\/ R ) <-> -. v .<_ ( ( P .\/ Q ) .\/ R ) ) )
23 22 rspcev 
 |-  ( ( v e. A /\ -. v .<_ ( ( P .\/ Q ) .\/ R ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
24 6 20 23 syl2anc 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P = Q ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
25 simp2l 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> v e. A )
26 25 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ R ) ) -> v e. A )
27 7 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ R ) ) -> -. v .<_ ( Q .\/ R ) )
28 1 3 hlatjass 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ Q ) .\/ R ) = ( P .\/ ( Q .\/ R ) ) )
29 28 3ad2ant1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> ( ( P .\/ Q ) .\/ R ) = ( P .\/ ( Q .\/ R ) ) )
30 29 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ R ) ) -> ( ( P .\/ Q ) .\/ R ) = ( P .\/ ( Q .\/ R ) ) )
31 8 hllatd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> K e. Lat )
32 simp1r1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> P e. A )
33 eqid 
 |-  ( Base ` K ) = ( Base ` K )
34 33 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
35 32 34 syl 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> P e. ( Base ` K ) )
36 simp1r3 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> R e. A )
37 33 1 3 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
38 8 9 36 37 syl3anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
39 31 35 38 3jca 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> ( K e. Lat /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) )
40 39 adantr 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) -> ( K e. Lat /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) )
41 33 2 1 latleeqj1 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) -> ( P .<_ ( Q .\/ R ) <-> ( P .\/ ( Q .\/ R ) ) = ( Q .\/ R ) ) )
42 40 41 syl 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) -> ( P .<_ ( Q .\/ R ) <-> ( P .\/ ( Q .\/ R ) ) = ( Q .\/ R ) ) )
43 42 biimpa 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ R ) ) -> ( P .\/ ( Q .\/ R ) ) = ( Q .\/ R ) )
44 30 43 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ R ) ) -> ( ( P .\/ Q ) .\/ R ) = ( Q .\/ R ) )
45 44 breq2d 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ R ) ) -> ( v .<_ ( ( P .\/ Q ) .\/ R ) <-> v .<_ ( Q .\/ R ) ) )
46 27 45 mtbird 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ R ) ) -> -. v .<_ ( ( P .\/ Q ) .\/ R ) )
47 26 46 23 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ P .<_ ( Q .\/ R ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
48 simpl2r 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) -> w e. A )
49 48 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) -> w e. A )
50 8 32 9 3jca 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
51 50 ad3antrrr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
52 36 25 jca 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> ( R e. A /\ v e. A ) )
53 52 ad3antrrr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) -> ( R e. A /\ v e. A ) )
54 simpl3r 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) -> -. w .<_ ( ( Q .\/ R ) .\/ v ) )
55 54 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) -> -. w .<_ ( ( Q .\/ R ) .\/ v ) )
56 simplr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) -> -. P .<_ ( Q .\/ R ) )
57 simpr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) -> P .<_ ( ( Q .\/ R ) .\/ v ) )
58 1 2 3 3dimlem3a 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ v e. A ) /\ ( -. w .<_ ( ( Q .\/ R ) .\/ v ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> -. w .<_ ( ( P .\/ Q ) .\/ R ) )
59 51 53 55 56 57 58 syl113anc 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) -> -. w .<_ ( ( P .\/ Q ) .\/ R ) )
60 breq1 
 |-  ( s = w -> ( s .<_ ( ( P .\/ Q ) .\/ R ) <-> w .<_ ( ( P .\/ Q ) .\/ R ) ) )
61 60 notbid 
 |-  ( s = w -> ( -. s .<_ ( ( P .\/ Q ) .\/ R ) <-> -. w .<_ ( ( P .\/ Q ) .\/ R ) ) )
62 61 rspcev 
 |-  ( ( w e. A /\ -. w .<_ ( ( P .\/ Q ) .\/ R ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
63 49 59 62 syl2anc 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ P .<_ ( ( Q .\/ R ) .\/ v ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
64 simpl2l 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) -> v e. A )
65 64 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) -> v e. A )
66 50 ad3antrrr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
67 52 ad3antrrr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) -> ( R e. A /\ v e. A ) )
68 simpl3l 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) -> -. v .<_ ( Q .\/ R ) )
69 68 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) -> -. v .<_ ( Q .\/ R ) )
70 simplr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) -> -. P .<_ ( Q .\/ R ) )
71 simpr 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) -> -. P .<_ ( ( Q .\/ R ) .\/ v ) )
72 1 2 3 3dimlem4a 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ v e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. P .<_ ( Q .\/ R ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> -. v .<_ ( ( P .\/ Q ) .\/ R ) )
73 66 67 69 70 71 72 syl113anc 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) -> -. v .<_ ( ( P .\/ Q ) .\/ R ) )
74 65 73 23 syl2anc 
 |-  ( ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) /\ -. P .<_ ( ( Q .\/ R ) .\/ v ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
75 63 74 pm2.61dan 
 |-  ( ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) /\ -. P .<_ ( Q .\/ R ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
76 47 75 pm2.61dan 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) /\ P =/= Q ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
77 24 76 pm2.61dane 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( v e. A /\ w e. A ) /\ ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )
78 77 3exp 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( v e. A /\ w e. A ) -> ( ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) ) ) )
79 78 rexlimdvv 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( E. v e. A E. w e. A ( -. v .<_ ( Q .\/ R ) /\ -. w .<_ ( ( Q .\/ R ) .\/ v ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) ) )
80 5 79 mpd 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> E. s e. A -. s .<_ ( ( P .\/ Q ) .\/ R ) )