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

Metamath Proof Explorer

Theorem cdleme22eALTN

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