Metamath Proof Explorer

Theorem 3dim1

Description: Construct a 3-dimensional volume (height-4 element) on top of a given atom P . (Contributed by NM, 25-Jul-2012)

Ref Expression
Hypotheses 3dim0.j 
|- .\/ = ( join ` K )
3dim0.l 
|- .<_ = ( le ` K )
3dim0.a 
|- A = ( Atoms ` K )
Assertion 3dim1 
|- ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. 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 3dim0 
 |-  ( K e. HL -> E. t e. A E. u e. A E. v e. A E. w e. A ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) )
5 4 adantr 
 |-  ( ( K e. HL /\ P e. A ) -> E. t e. A E. u e. A E. v e. A E. w e. A ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) )
6 simpl2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P = t ) -> ( u e. A /\ v e. A /\ w e. A ) )
7 1 2 3 3dimlem1 
 |-  ( ( ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) /\ P = t ) -> ( P =/= u /\ -. v .<_ ( P .\/ u ) /\ -. w .<_ ( ( P .\/ u ) .\/ v ) ) )
8 7 3ad2antl3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P = t ) -> ( P =/= u /\ -. v .<_ ( P .\/ u ) /\ -. w .<_ ( ( P .\/ u ) .\/ v ) ) )
9 1 2 3 3dim1lem5 
 |-  ( ( ( u e. A /\ v e. A /\ w e. A ) /\ ( P =/= u /\ -. v .<_ ( P .\/ u ) /\ -. w .<_ ( ( P .\/ u ) .\/ v ) ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
10 6 8 9 syl2anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P = t ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
11 simp13 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> t e. A )
12 simp22 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> v e. A )
13 simp23 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> w e. A )
14 11 12 13 3jca 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( t e. A /\ v e. A /\ w e. A ) )
15 14 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) /\ P .<_ ( t .\/ u ) ) -> ( t e. A /\ v e. A /\ w e. A ) )
16 simpll1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) /\ P .<_ ( t .\/ u ) ) -> ( K e. HL /\ P e. A /\ t e. A ) )
17 simp21 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> u e. A )
18 simp32 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> -. v .<_ ( t .\/ u ) )
19 simp33 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> -. w .<_ ( ( t .\/ u ) .\/ v ) )
20 17 18 19 3jca 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( u e. A /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) )
21 20 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) /\ P .<_ ( t .\/ u ) ) -> ( u e. A /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) )
22 simplr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) /\ P .<_ ( t .\/ u ) ) -> P =/= t )
23 simpr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) /\ P .<_ ( t .\/ u ) ) -> P .<_ ( t .\/ u ) )
24 1 2 3 3dimlem2 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) /\ ( P =/= t /\ P .<_ ( t .\/ u ) ) ) -> ( P =/= t /\ -. v .<_ ( P .\/ t ) /\ -. w .<_ ( ( P .\/ t ) .\/ v ) ) )
25 16 21 22 23 24 syl112anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) /\ P .<_ ( t .\/ u ) ) -> ( P =/= t /\ -. v .<_ ( P .\/ t ) /\ -. w .<_ ( ( P .\/ t ) .\/ v ) ) )
26 1 2 3 3dim1lem5 
 |-  ( ( ( t e. A /\ v e. A /\ w e. A ) /\ ( P =/= t /\ -. v .<_ ( P .\/ t ) /\ -. w .<_ ( ( P .\/ t ) .\/ v ) ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
27 15 25 26 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) /\ P .<_ ( t .\/ u ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
28 11 17 13 3jca 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( t e. A /\ u e. A /\ w e. A ) )
29 28 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ P .<_ ( ( t .\/ u ) .\/ v ) ) -> ( t e. A /\ u e. A /\ w e. A ) )
30 simp1 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( K e. HL /\ P e. A /\ t e. A ) )
31 17 12 jca 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( u e. A /\ v e. A ) )
32 simp31 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> t =/= u )
33 32 19 jca 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( t =/= u /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) )
34 30 31 33 3jca 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A ) /\ ( t =/= u /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) )
35 34 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ P .<_ ( ( t .\/ u ) .\/ v ) ) -> ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A ) /\ ( t =/= u /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) )
36 simplrl 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ P .<_ ( ( t .\/ u ) .\/ v ) ) -> P =/= t )
37 simplrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ P .<_ ( ( t .\/ u ) .\/ v ) ) -> -. P .<_ ( t .\/ u ) )
38 simpr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ P .<_ ( ( t .\/ u ) .\/ v ) ) -> P .<_ ( ( t .\/ u ) .\/ v ) )
39 1 2 3 3dimlem3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A ) /\ ( t =/= u /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) /\ P .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( P =/= t /\ -. u .<_ ( P .\/ t ) /\ -. w .<_ ( ( P .\/ t ) .\/ u ) ) )
40 35 36 37 38 39 syl13anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ P .<_ ( ( t .\/ u ) .\/ v ) ) -> ( P =/= t /\ -. u .<_ ( P .\/ t ) /\ -. w .<_ ( ( P .\/ t ) .\/ u ) ) )
41 1 2 3 3dim1lem5 
 |-  ( ( ( t e. A /\ u e. A /\ w e. A ) /\ ( P =/= t /\ -. u .<_ ( P .\/ t ) /\ -. w .<_ ( ( P .\/ t ) .\/ u ) ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
42 29 40 41 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ P .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
43 11 17 12 3jca 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> ( t e. A /\ u e. A /\ v e. A ) )
44 43 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ -. P .<_ ( ( t .\/ u ) .\/ v ) ) -> ( t e. A /\ u e. A /\ v e. A ) )
45 simpl1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> ( K e. HL /\ P e. A /\ t e. A ) )
46 simpl21 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> u e. A )
47 simpl22 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> v e. A )
48 46 47 jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> ( u e. A /\ v e. A ) )
49 simpl31 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> t =/= u )
50 simpl32 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> -. v .<_ ( t .\/ u ) )
51 49 50 jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> ( t =/= u /\ -. v .<_ ( t .\/ u ) ) )
52 45 48 51 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) ) ) )
53 52 adantr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ -. P .<_ ( ( t .\/ u ) .\/ v ) ) -> ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) ) ) )
54 simplr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ -. P .<_ ( ( t .\/ u ) .\/ v ) ) -> ( P =/= t /\ -. P .<_ ( t .\/ u ) ) )
55 simpr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ -. P .<_ ( ( t .\/ u ) .\/ v ) ) -> -. P .<_ ( ( t .\/ u ) .\/ v ) )
56 1 2 3 3dimlem4 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) /\ -. P .<_ ( ( t .\/ u ) .\/ v ) ) -> ( P =/= t /\ -. u .<_ ( P .\/ t ) /\ -. v .<_ ( ( P .\/ t ) .\/ u ) ) )
57 53 54 55 56 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ -. P .<_ ( ( t .\/ u ) .\/ v ) ) -> ( P =/= t /\ -. u .<_ ( P .\/ t ) /\ -. v .<_ ( ( P .\/ t ) .\/ u ) ) )
58 1 2 3 3dim1lem5 
 |-  ( ( ( t e. A /\ u e. A /\ v e. A ) /\ ( P =/= t /\ -. u .<_ ( P .\/ t ) /\ -. v .<_ ( ( P .\/ t ) .\/ u ) ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
59 44 57 58 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) /\ -. P .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
60 42 59 pm2.61dan 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ ( P =/= t /\ -. P .<_ ( t .\/ u ) ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
61 60 anassrs 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) /\ -. P .<_ ( t .\/ u ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
62 27 61 pm2.61dan 
 |-  ( ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) /\ P =/= t ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
63 10 62 pm2.61dane 
 |-  ( ( ( K e. HL /\ P e. A /\ t e. A ) /\ ( u e. A /\ v e. A /\ w e. A ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )
64 63 3exp 
 |-  ( ( K e. HL /\ P e. A /\ t e. A ) -> ( ( u e. A /\ v e. A /\ w e. A ) -> ( ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) ) ) )
65 64 3expd 
 |-  ( ( K e. HL /\ P e. A /\ t e. A ) -> ( u e. A -> ( v e. A -> ( w e. A -> ( ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) ) ) ) ) )
66 65 3exp 
 |-  ( K e. HL -> ( P e. A -> ( t e. A -> ( u e. A -> ( v e. A -> ( w e. A -> ( ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) ) ) ) ) ) ) )
67 66 imp43 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( t e. A /\ u e. A ) ) -> ( v e. A -> ( w e. A -> ( ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) ) ) ) )
68 67 impd 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( t e. A /\ u e. A ) ) -> ( ( v e. A /\ w e. A ) -> ( ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) ) ) )
69 68 rexlimdvv 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( t e. A /\ u e. A ) ) -> ( E. v e. A E. w e. A ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) ) )
70 69 rexlimdvva 
 |-  ( ( K e. HL /\ P e. A ) -> ( E. t e. A E. u e. A E. v e. A E. w e. A ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ -. w .<_ ( ( t .\/ u ) .\/ v ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) ) )
71 5 70 mpd 
 |-  ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )