Metamath Proof Explorer

Theorem ps-2

Description: Lattice analogue for the projective geometry axiom, "if a line intersects two sides of a triangle at different points then it also intersects the third side." Projective space condition PS2 in MaedaMaeda p. 68 and part of Theorem 16.4 in MaedaMaeda p. 69. (Contributed by NM, 1-Dec-2011)

Ref Expression
Hypotheses ps1.l 
|- .<_ = ( le ` K )
ps1.j 
|- .\/ = ( join ` K )
ps1.a 
|- A = ( Atoms ` K )
Assertion ps-2 
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) )

Proof

Step Hyp Ref Expression
1 ps1.l 
 |-  .<_ = ( le ` K )
2 ps1.j 
 |-  .\/ = ( join ` K )
3 ps1.a 
 |-  A = ( Atoms ` K )
4 simpl21 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S = P ) -> P e. A )
5 simp1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> K e. HL )
6 simp21 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> P e. A )
7 simp23 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> R e. A )
8 1 2 3 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ R e. A ) -> P .<_ ( P .\/ R ) )
9 5 6 7 8 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> P .<_ ( P .\/ R ) )
10 9 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S = P ) -> P .<_ ( P .\/ R ) )
11 simp3r 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> T e. A )
12 1 2 3 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ T e. A ) -> P .<_ ( P .\/ T ) )
13 5 6 11 12 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> P .<_ ( P .\/ T ) )
14 oveq1 
 |-  ( S = P -> ( S .\/ T ) = ( P .\/ T ) )
15 14 breq2d 
 |-  ( S = P -> ( P .<_ ( S .\/ T ) <-> P .<_ ( P .\/ T ) ) )
16 13 15 syl5ibrcom 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( S = P -> P .<_ ( S .\/ T ) ) )
17 16 imp 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S = P ) -> P .<_ ( S .\/ T ) )
18 breq1 
 |-  ( u = P -> ( u .<_ ( P .\/ R ) <-> P .<_ ( P .\/ R ) ) )
19 breq1 
 |-  ( u = P -> ( u .<_ ( S .\/ T ) <-> P .<_ ( S .\/ T ) ) )
20 18 19 anbi12d 
 |-  ( u = P -> ( ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) <-> ( P .<_ ( P .\/ R ) /\ P .<_ ( S .\/ T ) ) ) )
21 20 rspcev 
 |-  ( ( P e. A /\ ( P .<_ ( P .\/ R ) /\ P .<_ ( S .\/ T ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) )
22 4 10 17 21 syl12anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S = P ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) )
23 22 a1d 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S = P ) -> ( ( ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) ) )
24 hlop 
 |-  ( K e. HL -> K e. OP )
25 24 3ad2ant1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> K e. OP )
26 eqid 
 |-  ( Base ` K ) = ( Base ` K )
27 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
28 26 27 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
29 25 28 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( 0. ` K ) e. ( Base ` K ) )
30 26 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
31 6 30 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> P e. ( Base ` K ) )
32 eqid 
 |-  (
33 27 32 3 atcvr0 
 |-  ( ( K e. HL /\ P e. A ) -> ( 0. ` K ) (
34 5 6 33 syl2anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( 0. ` K ) (
35 eqid 
 |-  ( lt ` K ) = ( lt ` K )
36 26 35 32 cvrlt 
 |-  ( ( ( K e. HL /\ ( 0. ` K ) e. ( Base ` K ) /\ P e. ( Base ` K ) ) /\ ( 0. ` K ) (  ( 0. ` K ) ( lt ` K ) P )
37 5 29 31 34 36 syl31anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( 0. ` K ) ( lt ` K ) P )
38 hlpos 
 |-  ( K e. HL -> K e. Poset )
39 38 3ad2ant1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> K e. Poset )
40 hllat 
 |-  ( K e. HL -> K e. Lat )
41 40 3ad2ant1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> K e. Lat )
42 26 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
43 7 42 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> R e. ( Base ` K ) )
44 26 2 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( P .\/ R ) e. ( Base ` K ) )
45 41 31 43 44 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( P .\/ R ) e. ( Base ` K ) )
46 26 1 35 pltletr 
 |-  ( ( K e. Poset /\ ( ( 0. ` K ) e. ( Base ` K ) /\ P e. ( Base ` K ) /\ ( P .\/ R ) e. ( Base ` K ) ) ) -> ( ( ( 0. ` K ) ( lt ` K ) P /\ P .<_ ( P .\/ R ) ) -> ( 0. ` K ) ( lt ` K ) ( P .\/ R ) ) )
47 39 29 31 45 46 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( ( 0. ` K ) ( lt ` K ) P /\ P .<_ ( P .\/ R ) ) -> ( 0. ` K ) ( lt ` K ) ( P .\/ R ) ) )
48 37 9 47 mp2and 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( 0. ` K ) ( lt ` K ) ( P .\/ R ) )
49 35 pltne 
 |-  ( ( K e. HL /\ ( 0. ` K ) e. ( Base ` K ) /\ ( P .\/ R ) e. ( Base ` K ) ) -> ( ( 0. ` K ) ( lt ` K ) ( P .\/ R ) -> ( 0. ` K ) =/= ( P .\/ R ) ) )
50 5 29 45 49 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( 0. ` K ) ( lt ` K ) ( P .\/ R ) -> ( 0. ` K ) =/= ( P .\/ R ) ) )
51 48 50 mpd 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( 0. ` K ) =/= ( P .\/ R ) )
52 51 necomd 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( P .\/ R ) =/= ( 0. ` K ) )
53 52 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> ( P .\/ R ) =/= ( 0. ` K ) )
54 hlatl 
 |-  ( K e. HL -> K e. AtLat )
55 54 3ad2ant1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> K e. AtLat )
56 simp3l 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> S e. A )
57 1 3 atncmp 
 |-  ( ( K e. AtLat /\ S e. A /\ P e. A ) -> ( -. S .<_ P <-> S =/= P ) )
58 55 56 6 57 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( -. S .<_ P <-> S =/= P ) )
59 simp22 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> Q e. A )
60 26 1 2 3 hlexch1 
 |-  ( ( K e. HL /\ ( S e. A /\ Q e. A /\ P e. ( Base ` K ) ) /\ -. S .<_ P ) -> ( S .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ S ) ) )
61 60 3expia 
 |-  ( ( K e. HL /\ ( S e. A /\ Q e. A /\ P e. ( Base ` K ) ) ) -> ( -. S .<_ P -> ( S .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ S ) ) ) )
62 5 56 59 31 61 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( -. S .<_ P -> ( S .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ S ) ) ) )
63 58 62 sylbird 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( S =/= P -> ( S .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ S ) ) ) )
64 63 imp32 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ S .<_ ( P .\/ Q ) ) ) -> Q .<_ ( P .\/ S ) )
65 26 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
66 59 65 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> Q e. ( Base ` K ) )
67 26 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
68 56 67 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> S e. ( Base ` K ) )
69 26 2 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( P .\/ S ) e. ( Base ` K ) )
70 41 31 68 69 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( P .\/ S ) e. ( Base ` K ) )
71 26 1 2 latjlej1 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) ) -> ( Q .<_ ( P .\/ S ) -> ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) ) )
72 41 66 70 43 71 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( Q .<_ ( P .\/ S ) -> ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) ) )
73 72 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ S .<_ ( P .\/ Q ) ) ) -> ( Q .<_ ( P .\/ S ) -> ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) ) )
74 64 73 mpd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ S .<_ ( P .\/ Q ) ) ) -> ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) )
75 74 adantrrr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) )
76 26 3 atbase 
 |-  ( T e. A -> T e. ( Base ` K ) )
77 11 76 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> T e. ( Base ` K ) )
78 26 2 latjcl 
 |-  ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
79 41 66 43 78 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
80 26 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ S ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( ( P .\/ S ) .\/ R ) e. ( Base ` K ) )
81 41 70 43 80 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( P .\/ S ) .\/ R ) e. ( Base ` K ) )
82 26 1 lattr 
 |-  ( ( K e. Lat /\ ( T e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) /\ ( ( P .\/ S ) .\/ R ) e. ( Base ` K ) ) ) -> ( ( T .<_ ( Q .\/ R ) /\ ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) ) -> T .<_ ( ( P .\/ S ) .\/ R ) ) )
83 41 77 79 81 82 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( T .<_ ( Q .\/ R ) /\ ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) ) -> T .<_ ( ( P .\/ S ) .\/ R ) ) )
84 83 expdimp 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ T .<_ ( Q .\/ R ) ) -> ( ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) -> T .<_ ( ( P .\/ S ) .\/ R ) ) )
85 84 adantrl 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) -> ( ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) -> T .<_ ( ( P .\/ S ) .\/ R ) ) )
86 85 adantrl 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> ( ( Q .\/ R ) .<_ ( ( P .\/ S ) .\/ R ) -> T .<_ ( ( P .\/ S ) .\/ R ) ) )
87 75 86 mpd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> T .<_ ( ( P .\/ S ) .\/ R ) )
88 2 3 hlatj32 
 |-  ( ( K e. HL /\ ( P e. A /\ S e. A /\ R e. A ) ) -> ( ( P .\/ S ) .\/ R ) = ( ( P .\/ R ) .\/ S ) )
89 5 6 56 7 88 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( P .\/ S ) .\/ R ) = ( ( P .\/ R ) .\/ S ) )
90 89 breq2d 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( T .<_ ( ( P .\/ S ) .\/ R ) <-> T .<_ ( ( P .\/ R ) .\/ S ) ) )
91 90 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> ( T .<_ ( ( P .\/ S ) .\/ R ) <-> T .<_ ( ( P .\/ R ) .\/ S ) ) )
92 87 91 mpbid 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> T .<_ ( ( P .\/ R ) .\/ S ) )
93 53 92 jca 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> ( ( P .\/ R ) =/= ( 0. ` K ) /\ T .<_ ( ( P .\/ R ) .\/ S ) ) )
94 93 adantrrl 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( S =/= P /\ ( -. P .<_ ( Q .\/ R ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) ) -> ( ( P .\/ R ) =/= ( 0. ` K ) /\ T .<_ ( ( P .\/ R ) .\/ S ) ) )
95 94 ex 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( S =/= P /\ ( -. P .<_ ( Q .\/ R ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> ( ( P .\/ R ) =/= ( 0. ` K ) /\ T .<_ ( ( P .\/ R ) .\/ S ) ) ) )
96 26 1 2 27 3 cvrat4 
 |-  ( ( K e. HL /\ ( ( P .\/ R ) e. ( Base ` K ) /\ T e. A /\ S e. A ) ) -> ( ( ( P .\/ R ) =/= ( 0. ` K ) /\ T .<_ ( ( P .\/ R ) .\/ S ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) ) )
97 5 45 11 56 96 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( ( P .\/ R ) =/= ( 0. ` K ) /\ T .<_ ( ( P .\/ R ) .\/ S ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) ) )
98 95 97 syld 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( S =/= P /\ ( -. P .<_ ( Q .\/ R ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) ) )
99 98 impl 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= P ) /\ ( -. P .<_ ( Q .\/ R ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) )
100 99 adantrlr 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= P ) /\ ( ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) )
101 1 3 atncmp 
 |-  ( ( K e. AtLat /\ T e. A /\ S e. A ) -> ( -. T .<_ S <-> T =/= S ) )
102 55 11 56 101 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( -. T .<_ S <-> T =/= S ) )
103 necom 
 |-  ( T =/= S <-> S =/= T )
104 102 103 bitrdi 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( -. T .<_ S <-> S =/= T ) )
105 104 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ u e. A ) -> ( -. T .<_ S <-> S =/= T ) )
106 simpl1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ u e. A ) -> K e. HL )
107 simpl3r 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ u e. A ) -> T e. A )
108 simpr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ u e. A ) -> u e. A )
109 68 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ u e. A ) -> S e. ( Base ` K ) )
110 26 1 2 3 hlexch1 
 |-  ( ( K e. HL /\ ( T e. A /\ u e. A /\ S e. ( Base ` K ) ) /\ -. T .<_ S ) -> ( T .<_ ( S .\/ u ) -> u .<_ ( S .\/ T ) ) )
111 110 3expia 
 |-  ( ( K e. HL /\ ( T e. A /\ u e. A /\ S e. ( Base ` K ) ) ) -> ( -. T .<_ S -> ( T .<_ ( S .\/ u ) -> u .<_ ( S .\/ T ) ) ) )
112 106 107 108 109 111 syl13anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ u e. A ) -> ( -. T .<_ S -> ( T .<_ ( S .\/ u ) -> u .<_ ( S .\/ T ) ) ) )
113 105 112 sylbird 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ u e. A ) -> ( S =/= T -> ( T .<_ ( S .\/ u ) -> u .<_ ( S .\/ T ) ) ) )
114 113 imp 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ u e. A ) /\ S =/= T ) -> ( T .<_ ( S .\/ u ) -> u .<_ ( S .\/ T ) ) )
115 114 an32s 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= T ) /\ u e. A ) -> ( T .<_ ( S .\/ u ) -> u .<_ ( S .\/ T ) ) )
116 115 anim2d 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= T ) /\ u e. A ) -> ( ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) -> ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) ) )
117 116 reximdva 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= T ) -> ( E. u e. A ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) ) )
118 117 ad2ant2rl 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= P ) /\ ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) ) -> ( E. u e. A ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) ) )
119 118 adantrr 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= P ) /\ ( ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> ( E. u e. A ( u .<_ ( P .\/ R ) /\ T .<_ ( S .\/ u ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) ) )
120 100 119 mpd 
 |-  ( ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= P ) /\ ( ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) )
121 120 ex 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ S =/= P ) -> ( ( ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) ) )
122 23 121 pm2.61dane 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) -> ( ( ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) ) )
123 122 imp 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( ( -. P .<_ ( Q .\/ R ) /\ S =/= T ) /\ ( S .<_ ( P .\/ Q ) /\ T .<_ ( Q .\/ R ) ) ) ) -> E. u e. A ( u .<_ ( P .\/ R ) /\ u .<_ ( S .\/ T ) ) )