Metamath Proof Explorer

Theorem cdleme22e

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 4th line on p. 115. F , N , O represent f(z), f_z(s), f_z(t) respectively. When t \/ v = p \/ q, f_z(s) <_ f_z(t) \/ v. (Contributed by NM, 6-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 )
cdleme22e.u 
|- U = ( ( P .\/ Q ) ./\ W )
cdleme22e.f 
|- F = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
cdleme22e.n 
|- N = ( ( P .\/ Q ) ./\ ( F .\/ ( ( S .\/ z ) ./\ W ) ) )
cdleme22e.o 
|- O = ( ( P .\/ Q ) ./\ ( F .\/ ( ( T .\/ z ) ./\ W ) ) )
Assertion cdleme22e 
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> N .<_ ( O .\/ V ) )

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 cdleme22e.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
7 cdleme22e.f 
 |-  F = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
8 cdleme22e.n 
 |-  N = ( ( P .\/ Q ) ./\ ( F .\/ ( ( S .\/ z ) ./\ W ) ) )
9 cdleme22e.o 
 |-  O = ( ( P .\/ Q ) ./\ ( F .\/ ( ( T .\/ z ) ./\ W ) ) )
10 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> K e. HL )
11 10 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> K e. Lat )
12 simp21l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> P e. A )
13 simp22l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> Q e. A )
14 eqid 
 |-  ( Base ` K ) = ( Base ` K )
15 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
16 10 12 13 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
17 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> W e. H )
18 simp33l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> z e. A )
19 1 2 3 4 5 6 7 14 cdleme1b 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ z e. A ) ) -> F e. ( Base ` K ) )
20 10 17 12 13 18 19 syl23anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> F e. ( Base ` K ) )
21 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> S e. A )
22 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ z e. A ) -> ( S .\/ z ) e. ( Base ` K ) )
23 10 21 18 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( S .\/ z ) e. ( Base ` K ) )
24 14 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
25 17 24 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> W e. ( Base ` K ) )
26 14 3 latmcl 
 |-  ( ( K e. Lat /\ ( S .\/ z ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( S .\/ z ) ./\ W ) e. ( Base ` K ) )
27 11 23 25 26 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( S .\/ z ) ./\ W ) e. ( Base ` K ) )
28 14 2 latjcl 
 |-  ( ( K e. Lat /\ F e. ( Base ` K ) /\ ( ( S .\/ z ) ./\ W ) e. ( Base ` K ) ) -> ( F .\/ ( ( S .\/ z ) ./\ W ) ) e. ( Base ` K ) )
29 11 20 27 28 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( F .\/ ( ( S .\/ z ) ./\ W ) ) e. ( Base ` K ) )
30 14 1 3 latmle1 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( F .\/ ( ( S .\/ z ) ./\ W ) ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( F .\/ ( ( S .\/ z ) ./\ W ) ) ) .<_ ( P .\/ Q ) )
31 11 16 29 30 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) ./\ ( F .\/ ( ( S .\/ z ) ./\ W ) ) ) .<_ ( P .\/ Q ) )
32 8 31 eqbrtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> N .<_ ( P .\/ Q ) )
33 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( K e. HL /\ W e. H ) )
34 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P e. A /\ -. P .<_ W ) )
35 simp23r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> T e. A )
36 simp31 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( V e. A /\ V .<_ W ) )
37 simp32l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> P =/= Q )
38 simp32r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( T .\/ V ) = ( P .\/ Q ) )
39 1 2 3 4 5 6 cdleme22a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ T e. A ) /\ ( ( V e. A /\ V .<_ W ) /\ P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) ) -> V = U )
40 33 34 13 35 36 37 38 39 syl133anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> V = U )
41 40 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( O .\/ V ) = ( O .\/ U ) )
42 9 oveq1i 
 |-  ( O .\/ U ) = ( ( ( P .\/ Q ) ./\ ( F .\/ ( ( T .\/ z ) ./\ W ) ) ) .\/ U )
43 simp21r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> -. P .<_ W )
44 1 2 3 4 5 6 cdleme0a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> U e. A )
45 10 17 12 43 13 37 44 syl222anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> U e. A )
46 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ z e. A ) -> ( T .\/ z ) e. ( Base ` K ) )
47 10 35 18 46 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( T .\/ z ) e. ( Base ` K ) )
48 14 3 latmcl 
 |-  ( ( K e. Lat /\ ( T .\/ z ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( T .\/ z ) ./\ W ) e. ( Base ` K ) )
49 11 47 25 48 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( T .\/ z ) ./\ W ) e. ( Base ` K ) )
50 14 2 latjcl 
 |-  ( ( K e. Lat /\ F e. ( Base ` K ) /\ ( ( T .\/ z ) ./\ W ) e. ( Base ` K ) ) -> ( F .\/ ( ( T .\/ z ) ./\ W ) ) e. ( Base ` K ) )
51 11 20 49 50 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( F .\/ ( ( T .\/ z ) ./\ W ) ) e. ( Base ` K ) )
52 1 2 3 4 5 6 cdlemeulpq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A ) ) -> U .<_ ( P .\/ Q ) )
53 10 17 12 13 52 syl22anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> U .<_ ( P .\/ Q ) )
54 14 1 2 3 4 atmod2i1 
 |-  ( ( K e. HL /\ ( U e. A /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( F .\/ ( ( T .\/ z ) ./\ W ) ) e. ( Base ` K ) ) /\ U .<_ ( P .\/ Q ) ) -> ( ( ( P .\/ Q ) ./\ ( F .\/ ( ( T .\/ z ) ./\ W ) ) ) .\/ U ) = ( ( P .\/ Q ) ./\ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) ) )
55 10 45 16 51 53 54 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( ( P .\/ Q ) ./\ ( F .\/ ( ( T .\/ z ) ./\ W ) ) ) .\/ U ) = ( ( P .\/ Q ) ./\ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) ) )
56 42 55 eqtr2id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) ./\ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) ) = ( O .\/ U ) )
57 41 56 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( O .\/ V ) = ( ( P .\/ Q ) ./\ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) ) )
58 40 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( T .\/ V ) = ( T .\/ U ) )
59 38 58 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ Q ) = ( T .\/ U ) )
60 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
61 10 35 45 60 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( T .\/ U ) e. ( Base ` K ) )
62 14 4 atbase 
 |-  ( z e. A -> z e. ( Base ` K ) )
63 18 62 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> z e. ( Base ` K ) )
64 14 1 2 latlej1 
 |-  ( ( K e. Lat /\ ( T .\/ U ) e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( T .\/ U ) .<_ ( ( T .\/ U ) .\/ z ) )
65 11 61 63 64 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( T .\/ U ) .<_ ( ( T .\/ U ) .\/ z ) )
66 2 4 hlatj32 
 |-  ( ( K e. HL /\ ( T e. A /\ U e. A /\ z e. A ) ) -> ( ( T .\/ U ) .\/ z ) = ( ( T .\/ z ) .\/ U ) )
67 10 35 45 18 66 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( T .\/ U ) .\/ z ) = ( ( T .\/ z ) .\/ U ) )
68 14 4 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
69 45 68 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> U e. ( Base ` K ) )
70 14 2 latj32 
 |-  ( ( K e. Lat /\ ( z e. ( Base ` K ) /\ U e. ( Base ` K ) /\ ( ( T .\/ z ) ./\ W ) e. ( Base ` K ) ) ) -> ( ( z .\/ U ) .\/ ( ( T .\/ z ) ./\ W ) ) = ( ( z .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) )
71 11 63 69 49 70 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( z .\/ U ) .\/ ( ( T .\/ z ) ./\ W ) ) = ( ( z .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) )
72 14 2 latj32 
 |-  ( ( K e. Lat /\ ( F e. ( Base ` K ) /\ ( ( T .\/ z ) ./\ W ) e. ( Base ` K ) /\ U e. ( Base ` K ) ) ) -> ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) = ( ( F .\/ U ) .\/ ( ( T .\/ z ) ./\ W ) ) )
73 11 20 49 69 72 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) = ( ( F .\/ U ) .\/ ( ( T .\/ z ) ./\ W ) ) )
74 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ z e. A ) -> ( P .\/ z ) e. ( Base ` K ) )
75 10 12 18 74 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ z ) e. ( Base ` K ) )
76 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ z e. A ) -> P .<_ ( P .\/ z ) )
77 10 12 18 76 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> P .<_ ( P .\/ z ) )
78 14 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( P e. A /\ ( P .\/ z ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ P .<_ ( P .\/ z ) ) -> ( P .\/ ( ( P .\/ z ) ./\ W ) ) = ( ( P .\/ z ) ./\ ( P .\/ W ) ) )
79 10 12 75 25 77 78 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ ( ( P .\/ z ) ./\ W ) ) = ( ( P .\/ z ) ./\ ( P .\/ W ) ) )
80 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
81 1 2 80 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ W ) = ( 1. ` K ) )
82 10 17 34 81 syl21anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ W ) = ( 1. ` K ) )
83 82 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ z ) ./\ ( P .\/ W ) ) = ( ( P .\/ z ) ./\ ( 1. ` K ) ) )
84 hlol 
 |-  ( K e. HL -> K e. OL )
85 10 84 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> K e. OL )
86 14 3 80 olm11 
 |-  ( ( K e. OL /\ ( P .\/ z ) e. ( Base ` K ) ) -> ( ( P .\/ z ) ./\ ( 1. ` K ) ) = ( P .\/ z ) )
87 85 75 86 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ z ) ./\ ( 1. ` K ) ) = ( P .\/ z ) )
88 79 83 87 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ ( ( P .\/ z ) ./\ W ) ) = ( P .\/ z ) )
89 88 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ ( ( P .\/ z ) ./\ W ) ) .\/ Q ) = ( ( P .\/ z ) .\/ Q ) )
90 6 oveq2i 
 |-  ( Q .\/ U ) = ( Q .\/ ( ( P .\/ Q ) ./\ W ) )
91 1 2 4 hlatlej2 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> Q .<_ ( P .\/ Q ) )
92 10 12 13 91 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> Q .<_ ( P .\/ Q ) )
93 14 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( Q e. A /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ Q .<_ ( P .\/ Q ) ) -> ( Q .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( P .\/ Q ) ./\ ( Q .\/ W ) ) )
94 10 13 16 25 92 93 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( Q .\/ ( ( P .\/ Q ) ./\ W ) ) = ( ( P .\/ Q ) ./\ ( Q .\/ W ) ) )
95 90 94 syl5eq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( Q .\/ U ) = ( ( P .\/ Q ) ./\ ( Q .\/ W ) ) )
96 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
97 1 2 80 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q .\/ W ) = ( 1. ` K ) )
98 10 17 96 97 syl21anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( Q .\/ W ) = ( 1. ` K ) )
99 98 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) ./\ ( Q .\/ W ) ) = ( ( P .\/ Q ) ./\ ( 1. ` K ) ) )
100 14 3 80 olm11 
 |-  ( ( K e. OL /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( 1. ` K ) ) = ( P .\/ Q ) )
101 85 16 100 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) ./\ ( 1. ` K ) ) = ( P .\/ Q ) )
102 95 99 101 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( Q .\/ U ) = ( P .\/ Q ) )
103 102 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( Q .\/ U ) .\/ ( ( P .\/ z ) ./\ W ) ) = ( ( P .\/ Q ) .\/ ( ( P .\/ z ) ./\ W ) ) )
104 14 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
105 12 104 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> P e. ( Base ` K ) )
106 14 3 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ z ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ z ) ./\ W ) e. ( Base ` K ) )
107 11 75 25 106 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ z ) ./\ W ) e. ( Base ` K ) )
108 14 4 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
109 13 108 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> Q e. ( Base ` K ) )
110 14 2 latj32 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ ( ( P .\/ z ) ./\ W ) e. ( Base ` K ) /\ Q e. ( Base ` K ) ) ) -> ( ( P .\/ ( ( P .\/ z ) ./\ W ) ) .\/ Q ) = ( ( P .\/ Q ) .\/ ( ( P .\/ z ) ./\ W ) ) )
111 11 105 107 109 110 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ ( ( P .\/ z ) ./\ W ) ) .\/ Q ) = ( ( P .\/ Q ) .\/ ( ( P .\/ z ) ./\ W ) ) )
112 103 111 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( Q .\/ U ) .\/ ( ( P .\/ z ) ./\ W ) ) = ( ( P .\/ ( ( P .\/ z ) ./\ W ) ) .\/ Q ) )
113 2 4 hlatj32 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ z e. A ) ) -> ( ( P .\/ Q ) .\/ z ) = ( ( P .\/ z ) .\/ Q ) )
114 10 12 13 18 113 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) .\/ z ) = ( ( P .\/ z ) .\/ Q ) )
115 89 112 114 3eqtr4rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) .\/ z ) = ( ( Q .\/ U ) .\/ ( ( P .\/ z ) ./\ W ) ) )
116 14 2 latj32 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ U e. ( Base ` K ) /\ ( ( P .\/ z ) ./\ W ) e. ( Base ` K ) ) ) -> ( ( Q .\/ U ) .\/ ( ( P .\/ z ) ./\ W ) ) = ( ( Q .\/ ( ( P .\/ z ) ./\ W ) ) .\/ U ) )
117 11 109 69 107 116 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( Q .\/ U ) .\/ ( ( P .\/ z ) ./\ W ) ) = ( ( Q .\/ ( ( P .\/ z ) ./\ W ) ) .\/ U ) )
118 115 117 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) .\/ z ) = ( ( Q .\/ ( ( P .\/ z ) ./\ W ) ) .\/ U ) )
119 118 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( z .\/ U ) ./\ ( ( P .\/ Q ) .\/ z ) ) = ( ( z .\/ U ) ./\ ( ( Q .\/ ( ( P .\/ z ) ./\ W ) ) .\/ U ) ) )
120 14 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ z ) e. ( Base ` K ) )
121 11 16 63 120 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) .\/ z ) e. ( Base ` K ) )
122 14 1 2 latlej2 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> z .<_ ( ( P .\/ Q ) .\/ z ) )
123 11 16 63 122 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> z .<_ ( ( P .\/ Q ) .\/ z ) )
124 14 1 2 3 4 atmod1i1 
 |-  ( ( K e. HL /\ ( z e. A /\ U e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ z ) e. ( Base ` K ) ) /\ z .<_ ( ( P .\/ Q ) .\/ z ) ) -> ( z .\/ ( U ./\ ( ( P .\/ Q ) .\/ z ) ) ) = ( ( z .\/ U ) ./\ ( ( P .\/ Q ) .\/ z ) ) )
125 10 18 69 121 123 124 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( z .\/ ( U ./\ ( ( P .\/ Q ) .\/ z ) ) ) = ( ( z .\/ U ) ./\ ( ( P .\/ Q ) .\/ z ) ) )
126 7 oveq1i 
 |-  ( F .\/ U ) = ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ U )
127 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ z e. A /\ U e. A ) -> ( z .\/ U ) e. ( Base ` K ) )
128 10 18 45 127 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( z .\/ U ) e. ( Base ` K ) )
129 14 2 latjcl 
 |-  ( ( K e. Lat /\ Q e. ( Base ` K ) /\ ( ( P .\/ z ) ./\ W ) e. ( Base ` K ) ) -> ( Q .\/ ( ( P .\/ z ) ./\ W ) ) e. ( Base ` K ) )
130 11 109 107 129 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( Q .\/ ( ( P .\/ z ) ./\ W ) ) e. ( Base ` K ) )
131 1 2 4 hlatlej2 
 |-  ( ( K e. HL /\ z e. A /\ U e. A ) -> U .<_ ( z .\/ U ) )
132 10 18 45 131 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> U .<_ ( z .\/ U ) )
133 14 1 2 3 4 atmod2i1 
 |-  ( ( K e. HL /\ ( U e. A /\ ( z .\/ U ) e. ( Base ` K ) /\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) e. ( Base ` K ) ) /\ U .<_ ( z .\/ U ) ) -> ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ U ) = ( ( z .\/ U ) ./\ ( ( Q .\/ ( ( P .\/ z ) ./\ W ) ) .\/ U ) ) )
134 10 45 128 130 132 133 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ U ) = ( ( z .\/ U ) ./\ ( ( Q .\/ ( ( P .\/ z ) ./\ W ) ) .\/ U ) ) )
135 126 134 syl5eq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( F .\/ U ) = ( ( z .\/ U ) ./\ ( ( Q .\/ ( ( P .\/ z ) ./\ W ) ) .\/ U ) ) )
136 119 125 135 3eqtr4rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( F .\/ U ) = ( z .\/ ( U ./\ ( ( P .\/ Q ) .\/ z ) ) ) )
137 14 1 2 latlej1 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ z ) )
138 11 16 63 137 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ z ) )
139 14 1 11 69 16 121 53 138 lattrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> U .<_ ( ( P .\/ Q ) .\/ z ) )
140 14 1 3 latleeqm1 
 |-  ( ( K e. Lat /\ U e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ z ) e. ( Base ` K ) ) -> ( U .<_ ( ( P .\/ Q ) .\/ z ) <-> ( U ./\ ( ( P .\/ Q ) .\/ z ) ) = U ) )
141 11 69 121 140 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( U .<_ ( ( P .\/ Q ) .\/ z ) <-> ( U ./\ ( ( P .\/ Q ) .\/ z ) ) = U ) )
142 139 141 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( U ./\ ( ( P .\/ Q ) .\/ z ) ) = U )
143 142 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( z .\/ ( U ./\ ( ( P .\/ Q ) .\/ z ) ) ) = ( z .\/ U ) )
144 136 143 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( F .\/ U ) = ( z .\/ U ) )
145 144 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( F .\/ U ) .\/ ( ( T .\/ z ) ./\ W ) ) = ( ( z .\/ U ) .\/ ( ( T .\/ z ) ./\ W ) ) )
146 73 145 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) = ( ( z .\/ U ) .\/ ( ( T .\/ z ) ./\ W ) ) )
147 1 2 4 hlatlej2 
 |-  ( ( K e. HL /\ T e. A /\ z e. A ) -> z .<_ ( T .\/ z ) )
148 10 35 18 147 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> z .<_ ( T .\/ z ) )
149 14 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( z e. A /\ ( T .\/ z ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ z .<_ ( T .\/ z ) ) -> ( z .\/ ( ( T .\/ z ) ./\ W ) ) = ( ( T .\/ z ) ./\ ( z .\/ W ) ) )
150 10 18 47 25 148 149 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( z .\/ ( ( T .\/ z ) ./\ W ) ) = ( ( T .\/ z ) ./\ ( z .\/ W ) ) )
151 simp33 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( z e. A /\ -. z .<_ W ) )
152 1 2 80 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( z e. A /\ -. z .<_ W ) ) -> ( z .\/ W ) = ( 1. ` K ) )
153 10 17 151 152 syl21anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( z .\/ W ) = ( 1. ` K ) )
154 153 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( T .\/ z ) ./\ ( z .\/ W ) ) = ( ( T .\/ z ) ./\ ( 1. ` K ) ) )
155 150 154 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( z .\/ ( ( T .\/ z ) ./\ W ) ) = ( ( T .\/ z ) ./\ ( 1. ` K ) ) )
156 14 3 80 olm11 
 |-  ( ( K e. OL /\ ( T .\/ z ) e. ( Base ` K ) ) -> ( ( T .\/ z ) ./\ ( 1. ` K ) ) = ( T .\/ z ) )
157 85 47 156 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( T .\/ z ) ./\ ( 1. ` K ) ) = ( T .\/ z ) )
158 155 157 eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( T .\/ z ) = ( z .\/ ( ( T .\/ z ) ./\ W ) ) )
159 158 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( T .\/ z ) .\/ U ) = ( ( z .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) )
160 71 146 159 3eqtr4rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( T .\/ z ) .\/ U ) = ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) )
161 67 160 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( T .\/ U ) .\/ z ) = ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) )
162 65 161 breqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( T .\/ U ) .<_ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) )
163 59 162 eqbrtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ Q ) .<_ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) )
164 14 2 latjcl 
 |-  ( ( K e. Lat /\ ( F .\/ ( ( T .\/ z ) ./\ W ) ) e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) e. ( Base ` K ) )
165 11 51 69 164 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) e. ( Base ` K ) )
166 14 1 3 latleeqm1 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) .<_ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) <-> ( ( P .\/ Q ) ./\ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) ) = ( P .\/ Q ) ) )
167 11 16 165 166 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) .<_ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) <-> ( ( P .\/ Q ) ./\ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) ) = ( P .\/ Q ) ) )
168 163 167 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( ( P .\/ Q ) ./\ ( ( F .\/ ( ( T .\/ z ) ./\ W ) ) .\/ U ) ) = ( P .\/ Q ) )
169 57 168 eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> ( P .\/ Q ) = ( O .\/ V ) )
170 32 169 breqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ T e. A ) ) /\ ( ( V e. A /\ V .<_ W ) /\ ( P =/= Q /\ ( T .\/ V ) = ( P .\/ Q ) ) /\ ( z e. A /\ -. z .<_ W ) ) ) -> N .<_ ( O .\/ V ) )