Metamath Proof Explorer

Theorem 4atlem11

Description: Lemma for 4at . Combine all three possible cases. (Contributed by NM, 10-Jul-2012)

Ref Expression
Hypotheses 4at.l 
|- .<_ = ( le ` K )
4at.j 
|- .\/ = ( join ` K )
4at.a 
|- A = ( Atoms ` K )
Assertion 4atlem11 
|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .\/ ( R .\/ S ) ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )

Proof

Step Hyp Ref Expression
1 4at.l 
 |-  .<_ = ( le ` K )
2 4at.j 
 |-  .\/ = ( join ` K )
3 4at.a 
 |-  A = ( Atoms ` K )
4 3anass 
 |-  ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) )
5 simpl11 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. HL )
6 5 hllatd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. Lat )
7 simpl2l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. A )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 8 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
10 7 9 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. ( Base ` K ) )
11 simpl2r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. A )
12 8 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
13 11 12 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. ( Base ` K ) )
14 simpl12 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P e. A )
15 simpl31 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> U e. A )
16 8 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ U e. A ) -> ( P .\/ U ) e. ( Base ` K ) )
17 5 14 15 16 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .\/ U ) e. ( Base ` K ) )
18 simpl32 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> V e. A )
19 simpl33 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> W e. A )
20 8 2 3 hlatjcl 
 |-  ( ( K e. HL /\ V e. A /\ W e. A ) -> ( V .\/ W ) e. ( Base ` K ) )
21 5 18 19 20 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( V .\/ W ) e. ( Base ` K ) )
22 8 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ U ) e. ( Base ` K ) /\ ( V .\/ W ) e. ( Base ` K ) ) -> ( ( P .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) )
23 6 17 21 22 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) )
24 8 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ S e. ( Base ` K ) /\ ( ( P .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) ) ) -> ( ( R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( R .\/ S ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
25 6 10 13 23 24 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( R .\/ S ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
26 25 anbi2d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) <-> ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) )
27 4 26 bitrid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) )
28 simpl13 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q e. A )
29 8 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
30 28 29 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q e. ( Base ` K ) )
31 8 2 3 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
32 5 7 11 31 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R .\/ S ) e. ( Base ` K ) )
33 8 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ ( R .\/ S ) e. ( Base ` K ) /\ ( ( P .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) ) ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( Q .\/ ( R .\/ S ) ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
34 6 30 32 23 33 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( Q .\/ ( R .\/ S ) ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
35 27 34 bitrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( Q .\/ ( R .\/ S ) ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
36 simpl1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
37 simpl2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R e. A /\ S e. A ) )
38 18 19 jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( V e. A /\ W e. A ) )
39 simpr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
40 1 2 3 4atlem3a 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. Q .<_ ( ( P .\/ V ) .\/ W ) \/ -. R .<_ ( ( P .\/ V ) .\/ W ) \/ -. S .<_ ( ( P .\/ V ) .\/ W ) ) )
41 36 37 38 39 40 syl31anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. Q .<_ ( ( P .\/ V ) .\/ W ) \/ -. R .<_ ( ( P .\/ V ) .\/ W ) \/ -. S .<_ ( ( P .\/ V ) .\/ W ) ) )
42 simp1l 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
43 simp1r 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
44 simp2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> -. Q .<_ ( ( P .\/ V ) .\/ W ) )
45 simp3 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
46 1 2 3 4atlem11b 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. Q .<_ ( ( P .\/ V ) .\/ W ) ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
47 42 43 44 45 46 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
48 47 3exp 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. Q .<_ ( ( P .\/ V ) .\/ W ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) )
49 5 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> K e. HL )
50 14 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> P e. A )
51 28 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> Q e. A )
52 7 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> R e. A )
53 11 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> S e. A )
54 2 3 hlatj4 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ R ) .\/ ( Q .\/ S ) ) )
55 49 50 51 52 53 54 syl122anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ R ) .\/ ( Q .\/ S ) ) )
56 49 50 52 3jca 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( K e. HL /\ P e. A /\ R e. A ) )
57 51 53 jca 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( Q e. A /\ S e. A ) )
58 simp1l3 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( U e. A /\ V e. A /\ W e. A ) )
59 simp1r2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> -. R .<_ ( P .\/ Q ) )
60 1 2 3 4atlem0be 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. R .<_ ( P .\/ Q ) ) -> P =/= R )
61 49 50 51 52 59 60 syl131anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> P =/= R )
62 simp1r1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> P =/= Q )
63 1 2 3 4atlem0ae 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> -. Q .<_ ( P .\/ R ) )
64 49 50 51 52 62 59 63 syl132anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> -. Q .<_ ( P .\/ R ) )
65 simp1r3 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> -. S .<_ ( ( P .\/ Q ) .\/ R ) )
66 2 3 hlatj32 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( P .\/ R ) .\/ Q ) )
67 49 50 51 52 66 syl13anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( P .\/ R ) .\/ Q ) )
68 67 breq2d 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ R ) <-> S .<_ ( ( P .\/ R ) .\/ Q ) ) )
69 65 68 mtbid 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> -. S .<_ ( ( P .\/ R ) .\/ Q ) )
70 61 64 69 3jca 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( P =/= R /\ -. Q .<_ ( P .\/ R ) /\ -. S .<_ ( ( P .\/ R ) .\/ Q ) ) )
71 simp2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> -. R .<_ ( ( P .\/ V ) .\/ W ) )
72 simp32 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
73 simp31 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
74 simp33 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
75 1 2 3 4atlem11b 
 |-  ( ( ( ( K e. HL /\ P e. A /\ R e. A ) /\ ( Q e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= R /\ -. Q .<_ ( P .\/ R ) /\ -. S .<_ ( ( P .\/ R ) .\/ Q ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) ) /\ ( R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ R ) .\/ ( Q .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
76 56 57 58 70 71 72 73 74 75 syl323anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ R ) .\/ ( Q .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
77 55 76 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
78 77 3exp 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. R .<_ ( ( P .\/ V ) .\/ W ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) )
79 8 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
80 14 79 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P e. ( Base ` K ) )
81 8 2 latj4rot 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) /\ ( R e. ( Base ` K ) /\ S e. ( Base ` K ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( S .\/ P ) .\/ ( Q .\/ R ) ) )
82 6 80 30 10 13 81 syl122anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( S .\/ P ) .\/ ( Q .\/ R ) ) )
83 2 3 hlatjcom 
 |-  ( ( K e. HL /\ S e. A /\ P e. A ) -> ( S .\/ P ) = ( P .\/ S ) )
84 5 11 14 83 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S .\/ P ) = ( P .\/ S ) )
85 84 oveq1d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( S .\/ P ) .\/ ( Q .\/ R ) ) = ( ( P .\/ S ) .\/ ( Q .\/ R ) ) )
86 82 85 eqtrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ S ) .\/ ( Q .\/ R ) ) )
87 86 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ S ) .\/ ( Q .\/ R ) ) )
88 5 14 11 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( K e. HL /\ P e. A /\ S e. A ) )
89 28 7 jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( Q e. A /\ R e. A ) )
90 simpl3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( U e. A /\ V e. A /\ W e. A ) )
91 88 89 90 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( K e. HL /\ P e. A /\ S e. A ) /\ ( Q e. A /\ R e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
92 91 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( K e. HL /\ P e. A /\ S e. A ) /\ ( Q e. A /\ R e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
93 1 2 3 4noncolr1 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S =/= P /\ -. Q .<_ ( S .\/ P ) /\ -. R .<_ ( ( S .\/ P ) .\/ Q ) ) )
94 36 37 39 93 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S =/= P /\ -. Q .<_ ( S .\/ P ) /\ -. R .<_ ( ( S .\/ P ) .\/ Q ) ) )
95 necom 
 |-  ( S =/= P <-> P =/= S )
96 95 a1i 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S =/= P <-> P =/= S ) )
97 84 breq2d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( Q .<_ ( S .\/ P ) <-> Q .<_ ( P .\/ S ) ) )
98 97 notbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. Q .<_ ( S .\/ P ) <-> -. Q .<_ ( P .\/ S ) ) )
99 84 oveq1d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( S .\/ P ) .\/ Q ) = ( ( P .\/ S ) .\/ Q ) )
100 99 breq2d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R .<_ ( ( S .\/ P ) .\/ Q ) <-> R .<_ ( ( P .\/ S ) .\/ Q ) ) )
101 100 notbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. R .<_ ( ( S .\/ P ) .\/ Q ) <-> -. R .<_ ( ( P .\/ S ) .\/ Q ) ) )
102 96 98 101 3anbi123d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( S =/= P /\ -. Q .<_ ( S .\/ P ) /\ -. R .<_ ( ( S .\/ P ) .\/ Q ) ) <-> ( P =/= S /\ -. Q .<_ ( P .\/ S ) /\ -. R .<_ ( ( P .\/ S ) .\/ Q ) ) ) )
103 94 102 mpbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P =/= S /\ -. Q .<_ ( P .\/ S ) /\ -. R .<_ ( ( P .\/ S ) .\/ Q ) ) )
104 103 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( P =/= S /\ -. Q .<_ ( P .\/ S ) /\ -. R .<_ ( ( P .\/ S ) .\/ Q ) ) )
105 simp2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> -. S .<_ ( ( P .\/ V ) .\/ W ) )
106 simpr3 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
107 simpr1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
108 simpr2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
109 106 107 108 3jca 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
110 109 3adant2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
111 1 2 3 4atlem11b 
 |-  ( ( ( ( K e. HL /\ P e. A /\ S e. A ) /\ ( Q e. A /\ R e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= S /\ -. Q .<_ ( P .\/ S ) /\ -. R .<_ ( ( P .\/ S ) .\/ Q ) ) /\ -. S .<_ ( ( P .\/ V ) .\/ W ) ) /\ ( S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ S ) .\/ ( Q .\/ R ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
112 92 104 105 110 111 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ S ) .\/ ( Q .\/ R ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
113 87 112 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( P .\/ V ) .\/ W ) /\ ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
114 113 3exp 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. S .<_ ( ( P .\/ V ) .\/ W ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) )
115 48 78 114 3jaod 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( -. Q .<_ ( ( P .\/ V ) .\/ W ) \/ -. R .<_ ( ( P .\/ V ) .\/ W ) \/ -. S .<_ ( ( P .\/ V ) .\/ W ) ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) ) )
116 41 115 mpd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )
117 35 116 sylbird 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .\/ ( R .\/ S ) ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) ) )