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

Metamath Proof Explorer

Theorem cdleme22b

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 5th line on p. 115. Show that t \/ v =/= p \/ q and s <_ p \/ q implies -. t <_ p \/ q. (Contributed by NM, 2-Dec-2012)

Ref Expression
Hypotheses cdleme22.l 
|- .<_ = ( le ` K )
cdleme22.j 
|- .\/ = ( join ` K )
cdleme22.m 
|- ./\ = ( meet ` K )
cdleme22.a 
|- A = ( Atoms ` K )
cdleme22.h 
|- H = ( LHyp ` K )
Assertion cdleme22b 
|- ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> -. T .<_ ( P .\/ Q ) )

Proof

Step Hyp Ref Expression
1 cdleme22.l 
 |-  .<_ = ( le ` K )
2 cdleme22.j 
 |-  .\/ = ( join ` K )
3 cdleme22.m 
 |-  ./\ = ( meet ` K )
4 cdleme22.a 
 |-  A = ( Atoms ` K )
5 cdleme22.h 
 |-  H = ( LHyp ` K )
6 simp1l 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> K e. HL )
7 simp1r1 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> S e. A )
8 simp1r2 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> T e. A )
9 simp1r3 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> S =/= T )
10 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
11 2 4 10 llni2 
 |-  ( ( ( K e. HL /\ S e. A /\ T e. A ) /\ S =/= T ) -> ( S .\/ T ) e. ( LLines ` K ) )
12 6 7 8 9 11 syl31anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( S .\/ T ) e. ( LLines ` K ) )
13 4 10 llnneat 
 |-  ( ( K e. HL /\ ( S .\/ T ) e. ( LLines ` K ) ) -> -. ( S .\/ T ) e. A )
14 6 12 13 syl2anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> -. ( S .\/ T ) e. A )
15 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
16 15 10 llnn0 
 |-  ( ( K e. HL /\ ( S .\/ T ) e. ( LLines ` K ) ) -> ( S .\/ T ) =/= ( 0. ` K ) )
17 6 12 16 syl2anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( S .\/ T ) =/= ( 0. ` K ) )
18 14 17 jca 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( -. ( S .\/ T ) e. A /\ ( S .\/ T ) =/= ( 0. ` K ) ) )
19 df-ne 
 |-  ( ( S .\/ T ) =/= ( 0. ` K ) <-> -. ( S .\/ T ) = ( 0. ` K ) )
20 19 anbi2i 
 |-  ( ( -. ( S .\/ T ) e. A /\ ( S .\/ T ) =/= ( 0. ` K ) ) <-> ( -. ( S .\/ T ) e. A /\ -. ( S .\/ T ) = ( 0. ` K ) ) )
21 pm4.56 
 |-  ( ( -. ( S .\/ T ) e. A /\ -. ( S .\/ T ) = ( 0. ` K ) ) <-> -. ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) )
22 20 21 bitri 
 |-  ( ( -. ( S .\/ T ) e. A /\ ( S .\/ T ) =/= ( 0. ` K ) ) <-> -. ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) )
23 18 22 sylib 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> -. ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) )
24 simp3r2 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> S .<_ ( T .\/ V ) )
25 simp3l 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> V e. A )
26 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ T e. A /\ V e. A ) -> T .<_ ( T .\/ V ) )
27 6 8 25 26 syl3anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> T .<_ ( T .\/ V ) )
28 6 hllatd 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> K e. Lat )
29 eqid 
 |-  ( Base ` K ) = ( Base ` K )
30 29 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
31 7 30 syl 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> S e. ( Base ` K ) )
32 29 4 atbase 
 |-  ( T e. A -> T e. ( Base ` K ) )
33 8 32 syl 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> T e. ( Base ` K ) )
34 29 2 4 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ V e. A ) -> ( T .\/ V ) e. ( Base ` K ) )
35 6 8 25 34 syl3anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( T .\/ V ) e. ( Base ` K ) )
36 29 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ T e. ( Base ` K ) /\ ( T .\/ V ) e. ( Base ` K ) ) ) -> ( ( S .<_ ( T .\/ V ) /\ T .<_ ( T .\/ V ) ) <-> ( S .\/ T ) .<_ ( T .\/ V ) ) )
37 28 31 33 35 36 syl13anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( S .<_ ( T .\/ V ) /\ T .<_ ( T .\/ V ) ) <-> ( S .\/ T ) .<_ ( T .\/ V ) ) )
38 24 27 37 mpbi2and 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( S .\/ T ) .<_ ( T .\/ V ) )
39 38 adantr 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ T .<_ ( P .\/ Q ) ) -> ( S .\/ T ) .<_ ( T .\/ V ) )
40 simp3r3 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> S .<_ ( P .\/ Q ) )
41 40 adantr 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ T .<_ ( P .\/ Q ) ) -> S .<_ ( P .\/ Q ) )
42 simpr 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ T .<_ ( P .\/ Q ) ) -> T .<_ ( P .\/ Q ) )
43 simp21 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> P e. A )
44 simp22 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> Q e. A )
45 29 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
46 6 43 44 45 syl3anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
47 29 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ T e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( S .<_ ( P .\/ Q ) /\ T .<_ ( P .\/ Q ) ) <-> ( S .\/ T ) .<_ ( P .\/ Q ) ) )
48 28 31 33 46 47 syl13anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( S .<_ ( P .\/ Q ) /\ T .<_ ( P .\/ Q ) ) <-> ( S .\/ T ) .<_ ( P .\/ Q ) ) )
49 48 adantr 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ T .<_ ( P .\/ Q ) ) -> ( ( S .<_ ( P .\/ Q ) /\ T .<_ ( P .\/ Q ) ) <-> ( S .\/ T ) .<_ ( P .\/ Q ) ) )
50 41 42 49 mpbi2and 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ T .<_ ( P .\/ Q ) ) -> ( S .\/ T ) .<_ ( P .\/ Q ) )
51 29 2 4 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
52 6 7 8 51 syl3anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( S .\/ T ) e. ( Base ` K ) )
53 29 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( ( S .\/ T ) e. ( Base ` K ) /\ ( T .\/ V ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( ( S .\/ T ) .<_ ( T .\/ V ) /\ ( S .\/ T ) .<_ ( P .\/ Q ) ) <-> ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) )
54 28 52 35 46 53 syl13anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( ( S .\/ T ) .<_ ( T .\/ V ) /\ ( S .\/ T ) .<_ ( P .\/ Q ) ) <-> ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) )
55 54 adantr 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ T .<_ ( P .\/ Q ) ) -> ( ( ( S .\/ T ) .<_ ( T .\/ V ) /\ ( S .\/ T ) .<_ ( P .\/ Q ) ) <-> ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) )
56 39 50 55 mpbi2and 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ T .<_ ( P .\/ Q ) ) -> ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) )
57 56 ex 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( T .<_ ( P .\/ Q ) -> ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) )
58 hlop 
 |-  ( K e. HL -> K e. OP )
59 6 58 syl 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> K e. OP )
60 59 adantr 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) ) -> K e. OP )
61 52 adantr 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) ) -> ( S .\/ T ) e. ( Base ` K ) )
62 simprl 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) ) -> ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A )
63 simprr 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) ) -> ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) )
64 29 1 15 4 leat3 
 |-  ( ( ( K e. OP /\ ( S .\/ T ) e. ( Base ` K ) /\ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A ) /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) -> ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) )
65 60 61 62 63 64 syl31anc 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) ) -> ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) )
66 65 exp32 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A -> ( ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) -> ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) ) ) )
67 breq2 
 |-  ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) = ( 0. ` K ) -> ( ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) <-> ( S .\/ T ) .<_ ( 0. ` K ) ) )
68 67 biimpa 
 |-  ( ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) = ( 0. ` K ) /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) -> ( S .\/ T ) .<_ ( 0. ` K ) )
69 29 1 15 ople0 
 |-  ( ( K e. OP /\ ( S .\/ T ) e. ( Base ` K ) ) -> ( ( S .\/ T ) .<_ ( 0. ` K ) <-> ( S .\/ T ) = ( 0. ` K ) ) )
70 59 52 69 syl2anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( S .\/ T ) .<_ ( 0. ` K ) <-> ( S .\/ T ) = ( 0. ` K ) ) )
71 68 70 imbitrid 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) = ( 0. ` K ) /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) -> ( S .\/ T ) = ( 0. ` K ) ) )
72 71 imp 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) = ( 0. ` K ) /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) ) -> ( S .\/ T ) = ( 0. ` K ) )
73 72 olcd 
 |-  ( ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) /\ ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) = ( 0. ` K ) /\ ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) ) ) -> ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) )
74 73 exp32 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) = ( 0. ` K ) -> ( ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) -> ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) ) ) )
75 simp3r1 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( T .\/ V ) =/= ( P .\/ Q ) )
76 2 3 15 4 2atmat0 
 |-  ( ( ( K e. HL /\ T e. A /\ V e. A ) /\ ( P e. A /\ Q e. A /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A \/ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) = ( 0. ` K ) ) )
77 6 8 25 43 44 75 76 syl33anc 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( ( T .\/ V ) ./\ ( P .\/ Q ) ) e. A \/ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) = ( 0. ` K ) ) )
78 66 74 77 mpjaod 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( ( S .\/ T ) .<_ ( ( T .\/ V ) ./\ ( P .\/ Q ) ) -> ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) ) )
79 57 78 syld 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> ( T .<_ ( P .\/ Q ) -> ( ( S .\/ T ) e. A \/ ( S .\/ T ) = ( 0. ` K ) ) ) )
80 23 79 mtod 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ S =/= T ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) ) ) -> -. T .<_ ( P .\/ Q ) )