Metamath Proof Explorer

Theorem dalawlem11

Description: Lemma for dalaw . First part of dalawlem13 . (Contributed by NM, 17-Sep-2012)

Ref Expression
Hypotheses dalawlem.l 
|- .<_ = ( le ` K )
dalawlem.j 
|- .\/ = ( join ` K )
dalawlem.m 
|- ./\ = ( meet ` K )
dalawlem.a 
|- A = ( Atoms ` K )
Assertion dalawlem11 
|- ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )

Proof

Step Hyp Ref Expression
1 dalawlem.l 
 |-  .<_ = ( le ` K )
2 dalawlem.j 
 |-  .\/ = ( join ` K )
3 dalawlem.m 
 |-  ./\ = ( meet ` K )
4 dalawlem.a 
 |-  A = ( Atoms ` K )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 simp11 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. HL )
7 6 hllatd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. Lat )
8 simp21 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> P e. A )
9 simp22 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q e. A )
10 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
11 6 8 9 10 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
12 simp31 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> S e. A )
13 simp32 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> T e. A )
14 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
15 6 12 13 14 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( S .\/ T ) e. ( Base ` K ) )
16 5 3 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. ( Base ` K ) )
17 7 11 15 16 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. ( Base ` K ) )
18 simp23 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> R e. A )
19 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
20 6 9 18 19 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
21 5 1 3 latmle1 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( P .\/ Q ) )
22 7 11 15 21 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( P .\/ Q ) )
23 simp12 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> P .<_ ( Q .\/ R ) )
24 5 4 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
25 9 24 syl 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q e. ( Base ` K ) )
26 5 4 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
27 18 26 syl 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> R e. ( Base ` K ) )
28 5 1 2 latlej1 
 |-  ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> Q .<_ ( Q .\/ R ) )
29 7 25 27 28 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q .<_ ( Q .\/ R ) )
30 5 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
31 8 30 syl 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> P e. ( Base ` K ) )
32 5 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( Q .\/ R ) /\ Q .<_ ( Q .\/ R ) ) <-> ( P .\/ Q ) .<_ ( Q .\/ R ) ) )
33 7 31 25 20 32 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .<_ ( Q .\/ R ) /\ Q .<_ ( Q .\/ R ) ) <-> ( P .\/ Q ) .<_ ( Q .\/ R ) ) )
34 23 29 33 mpbi2and 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ Q ) .<_ ( Q .\/ R ) )
35 5 1 7 17 11 20 22 34 lattrd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( Q .\/ R ) )
36 5 4 atbase 
 |-  ( T e. A -> T e. ( Base ` K ) )
37 13 36 syl 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> T e. ( Base ` K ) )
38 5 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ T ) e. ( Base ` K ) )
39 7 11 37 38 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) .\/ T ) e. ( Base ` K ) )
40 5 3 latmcl 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) .\/ T ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) ) -> ( ( ( P .\/ Q ) .\/ T ) ./\ ( S .\/ T ) ) e. ( Base ` K ) )
41 7 39 15 40 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ T ) ./\ ( S .\/ T ) ) e. ( Base ` K ) )
42 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ P e. A ) -> ( R .\/ P ) e. ( Base ` K ) )
43 6 18 8 42 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( R .\/ P ) e. ( Base ` K ) )
44 simp33 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> U e. A )
45 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ U e. A /\ S e. A ) -> ( U .\/ S ) e. ( Base ` K ) )
46 6 44 12 45 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( U .\/ S ) e. ( Base ` K ) )
47 5 3 latmcl 
 |-  ( ( K e. Lat /\ ( R .\/ P ) e. ( Base ` K ) /\ ( U .\/ S ) e. ( Base ` K ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) )
48 7 43 46 47 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) )
49 5 4 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
50 44 49 syl 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> U e. ( Base ` K ) )
51 5 2 latjcl 
 |-  ( ( K e. Lat /\ ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) e. ( Base ` K ) )
52 7 48 50 51 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) e. ( Base ` K ) )
53 5 2 latjcl 
 |-  ( ( K e. Lat /\ ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) e. ( Base ` K ) )
54 7 52 37 53 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) e. ( Base ` K ) )
55 5 1 2 latlej1 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ T ) )
56 7 11 37 55 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ T ) )
57 5 1 3 latmlem1 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ T ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) ) ) -> ( ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ T ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( P .\/ Q ) .\/ T ) ./\ ( S .\/ T ) ) ) )
58 7 11 39 15 57 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ T ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( P .\/ Q ) .\/ T ) ./\ ( S .\/ T ) ) ) )
59 56 58 mpd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( P .\/ Q ) .\/ T ) ./\ ( S .\/ T ) ) )
60 5 1 2 latlej2 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> T .<_ ( ( P .\/ Q ) .\/ T ) )
61 7 11 37 60 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> T .<_ ( ( P .\/ Q ) .\/ T ) )
62 5 1 2 3 4 atmod2i2 
 |-  ( ( K e. HL /\ ( S e. A /\ ( ( P .\/ Q ) .\/ T ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) /\ T .<_ ( ( P .\/ Q ) .\/ T ) ) -> ( ( ( ( P .\/ Q ) .\/ T ) ./\ S ) .\/ T ) = ( ( ( P .\/ Q ) .\/ T ) ./\ ( S .\/ T ) ) )
63 6 12 39 37 61 62 syl131anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ T ) ./\ S ) .\/ T ) = ( ( ( P .\/ Q ) .\/ T ) ./\ ( S .\/ T ) ) )
64 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ T e. A ) -> ( Q .\/ T ) e. ( Base ` K ) )
65 6 9 13 64 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ T ) e. ( Base ` K ) )
66 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) e. ( Base ` K ) )
67 6 8 12 66 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ S ) e. ( Base ` K ) )
68 5 3 latmcom 
 |-  ( ( K e. Lat /\ ( Q .\/ T ) e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) = ( ( P .\/ S ) ./\ ( Q .\/ T ) ) )
69 7 65 67 68 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) = ( ( P .\/ S ) ./\ ( Q .\/ T ) ) )
70 simp13 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) )
71 69 70 eqbrtrd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) .<_ ( R .\/ U ) )
72 5 3 latmcl 
 |-  ( ( K e. Lat /\ ( Q .\/ T ) e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) e. ( Base ` K ) )
73 7 65 67 72 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) e. ( Base ` K ) )
74 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ U e. A ) -> ( R .\/ U ) e. ( Base ` K ) )
75 6 18 44 74 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( R .\/ U ) e. ( Base ` K ) )
76 5 1 2 latjlej2 
 |-  ( ( K e. Lat /\ ( ( ( Q .\/ T ) ./\ ( P .\/ S ) ) e. ( Base ` K ) /\ ( R .\/ U ) e. ( Base ` K ) /\ P e. ( Base ` K ) ) ) -> ( ( ( Q .\/ T ) ./\ ( P .\/ S ) ) .<_ ( R .\/ U ) -> ( P .\/ ( ( Q .\/ T ) ./\ ( P .\/ S ) ) ) .<_ ( P .\/ ( R .\/ U ) ) ) )
77 7 73 75 31 76 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( Q .\/ T ) ./\ ( P .\/ S ) ) .<_ ( R .\/ U ) -> ( P .\/ ( ( Q .\/ T ) ./\ ( P .\/ S ) ) ) .<_ ( P .\/ ( R .\/ U ) ) ) )
78 71 77 mpd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ ( ( Q .\/ T ) ./\ ( P .\/ S ) ) ) .<_ ( P .\/ ( R .\/ U ) ) )
79 5 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
80 12 79 syl 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> S e. ( Base ` K ) )
81 5 1 2 latlej1 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> P .<_ ( P .\/ S ) )
82 7 31 80 81 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> P .<_ ( P .\/ S ) )
83 5 1 2 3 4 atmod1i1 
 |-  ( ( K e. HL /\ ( P e. A /\ ( Q .\/ T ) e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) /\ P .<_ ( P .\/ S ) ) -> ( P .\/ ( ( Q .\/ T ) ./\ ( P .\/ S ) ) ) = ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) )
84 6 8 65 67 82 83 syl131anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ ( ( Q .\/ T ) ./\ ( P .\/ S ) ) ) = ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) )
85 2 4 hlatjass 
 |-  ( ( K e. HL /\ ( P e. A /\ R e. A /\ U e. A ) ) -> ( ( P .\/ R ) .\/ U ) = ( P .\/ ( R .\/ U ) ) )
86 6 8 18 44 85 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ R ) .\/ U ) = ( P .\/ ( R .\/ U ) ) )
87 2 4 hlatjcom 
 |-  ( ( K e. HL /\ P e. A /\ R e. A ) -> ( P .\/ R ) = ( R .\/ P ) )
88 6 8 18 87 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ R ) = ( R .\/ P ) )
89 88 oveq1d 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ R ) .\/ U ) = ( ( R .\/ P ) .\/ U ) )
90 86 89 eqtr3d 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ ( R .\/ U ) ) = ( ( R .\/ P ) .\/ U ) )
91 78 84 90 3brtr3d 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) .<_ ( ( R .\/ P ) .\/ U ) )
92 5 1 2 latlej2 
 |-  ( ( K e. Lat /\ U e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> S .<_ ( U .\/ S ) )
93 7 50 80 92 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> S .<_ ( U .\/ S ) )
94 5 2 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ ( Q .\/ T ) e. ( Base ` K ) ) -> ( P .\/ ( Q .\/ T ) ) e. ( Base ` K ) )
95 7 31 65 94 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ ( Q .\/ T ) ) e. ( Base ` K ) )
96 5 3 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ ( Q .\/ T ) ) e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) e. ( Base ` K ) )
97 7 95 67 96 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) e. ( Base ` K ) )
98 5 2 latjcl 
 |-  ( ( K e. Lat /\ ( R .\/ P ) e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> ( ( R .\/ P ) .\/ U ) e. ( Base ` K ) )
99 7 43 50 98 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( R .\/ P ) .\/ U ) e. ( Base ` K ) )
100 5 1 3 latmlem12 
 |-  ( ( K e. Lat /\ ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) e. ( Base ` K ) /\ ( ( R .\/ P ) .\/ U ) e. ( Base ` K ) ) /\ ( S e. ( Base ` K ) /\ ( U .\/ S ) e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) .<_ ( ( R .\/ P ) .\/ U ) /\ S .<_ ( U .\/ S ) ) -> ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) ./\ S ) .<_ ( ( ( R .\/ P ) .\/ U ) ./\ ( U .\/ S ) ) ) )
101 7 97 99 80 46 100 syl122anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) .<_ ( ( R .\/ P ) .\/ U ) /\ S .<_ ( U .\/ S ) ) -> ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) ./\ S ) .<_ ( ( ( R .\/ P ) .\/ U ) ./\ ( U .\/ S ) ) ) )
102 91 93 101 mp2and 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) ./\ S ) .<_ ( ( ( R .\/ P ) .\/ U ) ./\ ( U .\/ S ) ) )
103 hlol 
 |-  ( K e. HL -> K e. OL )
104 6 103 syl 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. OL )
105 5 3 latmassOLD 
 |-  ( ( K e. OL /\ ( ( P .\/ ( Q .\/ T ) ) e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) ) -> ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) ./\ S ) = ( ( P .\/ ( Q .\/ T ) ) ./\ ( ( P .\/ S ) ./\ S ) ) )
106 104 95 67 80 105 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) ./\ S ) = ( ( P .\/ ( Q .\/ T ) ) ./\ ( ( P .\/ S ) ./\ S ) ) )
107 2 4 hlatjass 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ T e. A ) ) -> ( ( P .\/ Q ) .\/ T ) = ( P .\/ ( Q .\/ T ) ) )
108 6 8 9 13 107 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) .\/ T ) = ( P .\/ ( Q .\/ T ) ) )
109 108 eqcomd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ ( Q .\/ T ) ) = ( ( P .\/ Q ) .\/ T ) )
110 5 1 2 latlej2 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> S .<_ ( P .\/ S ) )
111 7 31 80 110 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> S .<_ ( P .\/ S ) )
112 5 1 3 latleeqm2 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( S .<_ ( P .\/ S ) <-> ( ( P .\/ S ) ./\ S ) = S ) )
113 7 80 67 112 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( S .<_ ( P .\/ S ) <-> ( ( P .\/ S ) ./\ S ) = S ) )
114 111 113 mpbid 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ S ) ./\ S ) = S )
115 109 114 oveq12d 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ ( Q .\/ T ) ) ./\ ( ( P .\/ S ) ./\ S ) ) = ( ( ( P .\/ Q ) .\/ T ) ./\ S ) )
116 106 115 eqtr2d 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ T ) ./\ S ) = ( ( ( P .\/ ( Q .\/ T ) ) ./\ ( P .\/ S ) ) ./\ S ) )
117 5 1 2 latlej1 
 |-  ( ( K e. Lat /\ U e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> U .<_ ( U .\/ S ) )
118 7 50 80 117 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> U .<_ ( U .\/ S ) )
119 5 1 2 3 4 atmod4i1 
 |-  ( ( K e. HL /\ ( U e. A /\ ( R .\/ P ) e. ( Base ` K ) /\ ( U .\/ S ) e. ( Base ` K ) ) /\ U .<_ ( U .\/ S ) ) -> ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) = ( ( ( R .\/ P ) .\/ U ) ./\ ( U .\/ S ) ) )
120 6 44 43 46 118 119 syl131anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) = ( ( ( R .\/ P ) .\/ U ) ./\ ( U .\/ S ) ) )
121 102 116 120 3brtr4d 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ T ) ./\ S ) .<_ ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) )
122 5 3 latmcl 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) .\/ T ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( ( ( P .\/ Q ) .\/ T ) ./\ S ) e. ( Base ` K ) )
123 7 39 80 122 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ T ) ./\ S ) e. ( Base ` K ) )
124 5 1 2 latjlej1 
 |-  ( ( K e. Lat /\ ( ( ( ( P .\/ Q ) .\/ T ) ./\ S ) e. ( Base ` K ) /\ ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ Q ) .\/ T ) ./\ S ) .<_ ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) -> ( ( ( ( P .\/ Q ) .\/ T ) ./\ S ) .\/ T ) .<_ ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) ) )
125 7 123 52 37 124 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ T ) ./\ S ) .<_ ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) -> ( ( ( ( P .\/ Q ) .\/ T ) ./\ S ) .\/ T ) .<_ ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) ) )
126 121 125 mpd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ T ) ./\ S ) .\/ T ) .<_ ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) )
127 63 126 eqbrtrrd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ T ) ./\ ( S .\/ T ) ) .<_ ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) )
128 5 1 7 17 41 54 59 127 lattrd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) )
129 5 2 latj31 
 |-  ( ( K e. Lat /\ ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) /\ U e. ( Base ` K ) /\ T e. ( Base ` K ) ) ) -> ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) = ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
130 7 48 50 37 129 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ U ) .\/ T ) = ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
131 128 130 breqtrd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
132 5 2 4 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
133 6 13 44 132 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( T .\/ U ) e. ( Base ` K ) )
134 5 2 latjcl 
 |-  ( ( K e. Lat /\ ( T .\/ U ) e. ( Base ` K ) /\ ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) ) -> ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) e. ( Base ` K ) )
135 7 133 48 134 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) e. ( Base ` K ) )
136 5 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) /\ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( Q .\/ R ) /\ ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) <-> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( Q .\/ R ) ./\ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) ) )
137 7 17 20 135 136 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( Q .\/ R ) /\ ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) <-> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( Q .\/ R ) ./\ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) ) )
138 35 131 137 mpbi2and 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( Q .\/ R ) ./\ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) )
139 5 1 3 latmle1 
 |-  ( ( K e. Lat /\ ( R .\/ P ) e. ( Base ` K ) /\ ( U .\/ S ) e. ( Base ` K ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) .<_ ( R .\/ P ) )
140 7 43 46 139 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) .<_ ( R .\/ P ) )
141 5 1 2 latlej2 
 |-  ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> R .<_ ( Q .\/ R ) )
142 7 25 27 141 syl3anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> R .<_ ( Q .\/ R ) )
143 5 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) ) -> ( ( R .<_ ( Q .\/ R ) /\ P .<_ ( Q .\/ R ) ) <-> ( R .\/ P ) .<_ ( Q .\/ R ) ) )
144 7 27 31 20 143 syl13anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( R .<_ ( Q .\/ R ) /\ P .<_ ( Q .\/ R ) ) <-> ( R .\/ P ) .<_ ( Q .\/ R ) ) )
145 142 23 144 mpbi2and 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( R .\/ P ) .<_ ( Q .\/ R ) )
146 5 1 7 48 43 20 140 145 lattrd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) .<_ ( Q .\/ R ) )
147 5 1 2 3 4 llnmod2i2 
 |-  ( ( ( K e. HL /\ ( Q .\/ R ) e. ( Base ` K ) /\ ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) ) /\ ( T e. A /\ U e. A ) /\ ( ( R .\/ P ) ./\ ( U .\/ S ) ) .<_ ( Q .\/ R ) ) -> ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) = ( ( Q .\/ R ) ./\ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) )
148 6 20 48 13 44 146 147 syl321anc 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) = ( ( Q .\/ R ) ./\ ( ( T .\/ U ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) ) )
149 138 148 breqtrrd 
 |-  ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )