Metamath Proof Explorer

Theorem cdleme22cN

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 -. v <_ p \/ q. (Contributed by NM, 3-Dec-2012) (New usage is discouraged.)

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 cdleme22cN 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> -. V .<_ ( 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 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> K e. HL )
7 6 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> K e. Lat )
8 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> P e. A )
9 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> Q e. A )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
12 6 8 9 11 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
13 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> W e. H )
14 10 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
15 13 14 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> W e. ( Base ` K ) )
16 10 1 3 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
17 7 12 15 16 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
18 simp21r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> -. S .<_ W )
19 nbrne2 
 |-  ( ( ( ( P .\/ Q ) ./\ W ) .<_ W /\ -. S .<_ W ) -> ( ( P .\/ Q ) ./\ W ) =/= S )
20 17 18 19 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ W ) =/= S )
21 simp32l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> S .<_ ( T .\/ V ) )
22 21 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> S .<_ ( T .\/ V ) )
23 6 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> K e. HL )
24 13 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> W e. H )
25 simpl12 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> ( P e. A /\ -. P .<_ W ) )
26 simpl13 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> Q e. A )
27 simp31l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> P =/= Q )
28 27 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> P =/= Q )
29 simp23l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> V e. A )
30 29 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> V e. A )
31 simp23r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> V .<_ W )
32 31 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> V .<_ W )
33 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> V .<_ ( P .\/ Q ) )
34 eqid 
 |-  ( ( P .\/ Q ) ./\ W ) = ( ( P .\/ Q ) ./\ W )
35 1 2 3 4 5 34 cdleme22aa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V = ( ( P .\/ Q ) ./\ W ) )
36 23 24 25 26 28 30 32 33 35 syl233anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> V = ( ( P .\/ Q ) ./\ W ) )
37 36 oveq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> ( T .\/ V ) = ( T .\/ ( ( P .\/ Q ) ./\ W ) ) )
38 22 37 breqtrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> S .<_ ( T .\/ ( ( P .\/ Q ) ./\ W ) ) )
39 simp32r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> S .<_ ( P .\/ Q ) )
40 39 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> S .<_ ( P .\/ Q ) )
41 simp21l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> S e. A )
42 10 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
43 41 42 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> S e. ( Base ` K ) )
44 simp22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> T e. A )
45 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> -. P .<_ W )
46 1 2 3 4 5 lhpat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> ( ( P .\/ Q ) ./\ W ) e. A )
47 6 13 8 45 9 27 46 syl222anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ W ) e. A )
48 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ ( ( P .\/ Q ) ./\ W ) e. A ) -> ( T .\/ ( ( P .\/ Q ) ./\ W ) ) e. ( Base ` K ) )
49 6 44 47 48 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( T .\/ ( ( P .\/ Q ) ./\ W ) ) e. ( Base ` K ) )
50 10 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ ( T .\/ ( ( P .\/ Q ) ./\ W ) ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( S .<_ ( T .\/ ( ( P .\/ Q ) ./\ W ) ) /\ S .<_ ( P .\/ Q ) ) <-> S .<_ ( ( T .\/ ( ( P .\/ Q ) ./\ W ) ) ./\ ( P .\/ Q ) ) ) )
51 7 43 49 12 50 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( S .<_ ( T .\/ ( ( P .\/ Q ) ./\ W ) ) /\ S .<_ ( P .\/ Q ) ) <-> S .<_ ( ( T .\/ ( ( P .\/ Q ) ./\ W ) ) ./\ ( P .\/ Q ) ) ) )
52 51 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> ( ( S .<_ ( T .\/ ( ( P .\/ Q ) ./\ W ) ) /\ S .<_ ( P .\/ Q ) ) <-> S .<_ ( ( T .\/ ( ( P .\/ Q ) ./\ W ) ) ./\ ( P .\/ Q ) ) ) )
53 38 40 52 mpbi2and 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> S .<_ ( ( T .\/ ( ( P .\/ Q ) ./\ W ) ) ./\ ( P .\/ Q ) ) )
54 simp31r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> S =/= T )
55 41 44 54 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( S e. A /\ T e. A /\ S =/= T ) )
56 simp33 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( T .\/ V ) =/= ( P .\/ Q ) )
57 56 21 39 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( T .\/ V ) =/= ( P .\/ Q ) /\ S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) )
58 1 2 3 4 5 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 ) )
59 6 55 8 9 27 29 57 58 syl232anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> -. T .<_ ( P .\/ Q ) )
60 hlatl 
 |-  ( K e. HL -> K e. AtLat )
61 6 60 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> K e. AtLat )
62 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
63 10 1 3 62 4 atnle 
 |-  ( ( K e. AtLat /\ T e. A /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( -. T .<_ ( P .\/ Q ) <-> ( T ./\ ( P .\/ Q ) ) = ( 0. ` K ) ) )
64 61 44 12 63 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( -. T .<_ ( P .\/ Q ) <-> ( T ./\ ( P .\/ Q ) ) = ( 0. ` K ) ) )
65 59 64 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( T ./\ ( P .\/ Q ) ) = ( 0. ` K ) )
66 65 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( T ./\ ( P .\/ Q ) ) .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( 0. ` K ) .\/ ( ( P .\/ Q ) ./\ W ) ) )
67 10 4 atbase 
 |-  ( T e. A -> T e. ( Base ` K ) )
68 44 67 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> T e. ( Base ` K ) )
69 10 1 3 latmle1 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ ( P .\/ Q ) )
70 7 12 15 69 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ ( P .\/ Q ) )
71 10 1 2 3 4 atmod4i1 
 |-  ( ( K e. HL /\ ( ( ( P .\/ Q ) ./\ W ) e. A /\ T e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) /\ ( ( P .\/ Q ) ./\ W ) .<_ ( P .\/ Q ) ) -> ( ( T ./\ ( P .\/ Q ) ) .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( T .\/ ( ( P .\/ Q ) ./\ W ) ) ./\ ( P .\/ Q ) ) )
72 6 47 68 12 70 71 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( T ./\ ( P .\/ Q ) ) .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( T .\/ ( ( P .\/ Q ) ./\ W ) ) ./\ ( P .\/ Q ) ) )
73 hlol 
 |-  ( K e. HL -> K e. OL )
74 6 73 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> K e. OL )
75 10 3 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) e. ( Base ` K ) )
76 7 12 15 75 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ W ) e. ( Base ` K ) )
77 10 2 62 olj02 
 |-  ( ( K e. OL /\ ( ( P .\/ Q ) ./\ W ) e. ( Base ` K ) ) -> ( ( 0. ` K ) .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( P .\/ Q ) ./\ W ) )
78 74 76 77 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( 0. ` K ) .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( P .\/ Q ) ./\ W ) )
79 66 72 78 3eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( T .\/ ( ( P .\/ Q ) ./\ W ) ) ./\ ( P .\/ Q ) ) = ( ( P .\/ Q ) ./\ W ) )
80 79 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> ( ( T .\/ ( ( P .\/ Q ) ./\ W ) ) ./\ ( P .\/ Q ) ) = ( ( P .\/ Q ) ./\ W ) )
81 53 80 breqtrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> S .<_ ( ( P .\/ Q ) ./\ W ) )
82 1 4 atcmp 
 |-  ( ( K e. AtLat /\ S e. A /\ ( ( P .\/ Q ) ./\ W ) e. A ) -> ( S .<_ ( ( P .\/ Q ) ./\ W ) <-> S = ( ( P .\/ Q ) ./\ W ) ) )
83 61 41 47 82 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( S .<_ ( ( P .\/ Q ) ./\ W ) <-> S = ( ( P .\/ Q ) ./\ W ) ) )
84 83 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> ( S .<_ ( ( P .\/ Q ) ./\ W ) <-> S = ( ( P .\/ Q ) ./\ W ) ) )
85 81 84 mpbid 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> S = ( ( P .\/ Q ) ./\ W ) )
86 85 eqcomd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) /\ V .<_ ( P .\/ Q ) ) -> ( ( P .\/ Q ) ./\ W ) = S )
87 86 ex 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( V .<_ ( P .\/ Q ) -> ( ( P .\/ Q ) ./\ W ) = S ) )
88 87 necon3ad 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> ( ( ( P .\/ Q ) ./\ W ) =/= S -> -. V .<_ ( P .\/ Q ) ) )
89 20 88 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ -. S .<_ W ) /\ T e. A /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( S .<_ ( T .\/ V ) /\ S .<_ ( P .\/ Q ) ) /\ ( T .\/ V ) =/= ( P .\/ Q ) ) ) -> -. V .<_ ( P .\/ Q ) )