Metamath Proof Explorer

Theorem 4atlem10

Description: Lemma for 4at . Combine both possible cases. (Contributed by NM, 9-Jul-2012)

Ref Expression
Hypotheses 4at.l 
|- .<_ = ( le ` K )
4at.j 
|- .\/ = ( join ` K )
4at.a 
|- A = ( Atoms ` K )
Assertion 4atlem10 
|- ( ( ( 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 ) ) ) -> ( ( R .\/ S ) .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )

Proof

Step Hyp Ref Expression
1 4at.l 
 |-  .<_ = ( le ` K )
2 4at.j 
 |-  .\/ = ( join ` K )
3 4at.a 
 |-  A = ( Atoms ` K )
4 simp11 
 |-  ( ( ( 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 ) ) ) -> K e. HL )
5 4 hllatd 
 |-  ( ( ( 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 ) ) ) -> K e. Lat )
6 simp21l 
 |-  ( ( ( 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 ) ) ) -> R e. A )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
9 6 8 syl 
 |-  ( ( ( 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 ) ) ) -> R e. ( Base ` K ) )
10 simp21r 
 |-  ( ( ( 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 ) ) ) -> S e. A )
11 7 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
12 10 11 syl 
 |-  ( ( ( 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 ) ) ) -> S e. ( Base ` K ) )
13 7 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
14 13 3ad2ant1 
 |-  ( ( ( 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 ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
15 simp22 
 |-  ( ( ( 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 ) ) ) -> V e. A )
16 simp23 
 |-  ( ( ( 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 ) ) ) -> W e. A )
17 7 2 3 hlatjcl 
 |-  ( ( K e. HL /\ V e. A /\ W e. A ) -> ( V .\/ W ) e. ( Base ` K ) )
18 4 15 16 17 syl3anc 
 |-  ( ( ( 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 ) ) ) -> ( V .\/ W ) e. ( Base ` K ) )
19 7 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( V .\/ W ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ ( V .\/ W ) ) e. ( Base ` K ) )
20 5 14 18 19 syl3anc 
 |-  ( ( ( 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 ) ) ) -> ( ( P .\/ Q ) .\/ ( V .\/ W ) ) e. ( Base ` K ) )
21 7 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ S e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) e. ( Base ` K ) ) ) -> ( ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) <-> ( R .\/ S ) .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )
22 5 9 12 20 21 syl13anc 
 |-  ( ( ( 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 ) ) ) -> ( ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) <-> ( R .\/ S ) .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )
23 simp11 
 |-  ( ( ( ( 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 ) ) ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
24 6 10 15 3jca 
 |-  ( ( ( 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 ) ) ) -> ( R e. A /\ S e. A /\ V e. A ) )
25 24 3ad2ant1 
 |-  ( ( ( ( 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 ) ) ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( R e. A /\ S e. A /\ V e. A ) )
26 16 3ad2ant1 
 |-  ( ( ( ( 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 ) ) ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> W e. A )
27 simp2 
 |-  ( ( ( ( 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 ) ) ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> -. R .<_ ( ( P .\/ Q ) .\/ W ) )
28 simp33 
 |-  ( ( ( 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 ) ) ) -> -. S .<_ ( ( P .\/ Q ) .\/ R ) )
29 28 3ad2ant1 
 |-  ( ( ( ( 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 ) ) ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> -. S .<_ ( ( P .\/ Q ) .\/ R ) )
30 26 27 29 3jca 
 |-  ( ( ( ( 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 ) ) ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
31 simp3 
 |-  ( ( ( ( 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 ) ) ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )
32 1 2 3 4atlem10b 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
33 23 25 30 31 32 syl31anc 
 |-  ( ( ( ( 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 ) ) ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
34 33 3exp 
 |-  ( ( ( 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 ) ) ) -> ( -. R .<_ ( ( P .\/ Q ) .\/ W ) -> ( ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) )
35 2 3 hlatjcom 
 |-  ( ( K e. HL /\ S e. A /\ R e. A ) -> ( S .\/ R ) = ( R .\/ S ) )
36 4 10 6 35 syl3anc 
 |-  ( ( ( 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 ) ) ) -> ( S .\/ R ) = ( R .\/ S ) )
37 36 oveq2d 
 |-  ( ( ( 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 ) ) ) -> ( ( P .\/ Q ) .\/ ( S .\/ R ) ) = ( ( P .\/ Q ) .\/ ( R .\/ S ) ) )
38 37 3ad2ant1 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( S .\/ R ) ) = ( ( P .\/ Q ) .\/ ( R .\/ S ) ) )
39 simp11 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
40 10 6 15 3jca 
 |-  ( ( ( 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 ) ) ) -> ( S e. A /\ R e. A /\ V e. A ) )
41 40 3ad2ant1 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( S e. A /\ R e. A /\ V e. A ) )
42 16 3ad2ant1 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> W e. A )
43 simp2 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> -. S .<_ ( ( P .\/ Q ) .\/ W ) )
44 simp12 
 |-  ( ( ( 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 ) ) ) -> P e. A )
45 simp13 
 |-  ( ( ( 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 e. A )
46 44 45 jca 
 |-  ( ( ( 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 ) ) ) -> ( P e. A /\ Q e. A ) )
47 simp21 
 |-  ( ( ( 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 ) ) ) -> ( R e. A /\ S e. A ) )
48 simp32 
 |-  ( ( ( 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 ) ) ) -> -. R .<_ ( P .\/ Q ) )
49 1 2 3 4atlem0a 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> -. R .<_ ( ( P .\/ Q ) .\/ S ) )
50 4 46 47 48 28 49 syl32anc 
 |-  ( ( ( 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 ) ) ) -> -. R .<_ ( ( P .\/ Q ) .\/ S ) )
51 50 3ad2ant1 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> -. R .<_ ( ( P .\/ Q ) .\/ S ) )
52 42 43 51 3jca 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( W e. A /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ -. R .<_ ( ( P .\/ Q ) .\/ S ) ) )
53 simprr 
 |-  ( ( ( ( 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 ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
54 simprl 
 |-  ( ( ( ( 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 ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
55 53 54 jca 
 |-  ( ( ( ( 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 ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )
56 55 3adant2 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )
57 1 2 3 4atlem10b 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ R e. A /\ V e. A ) /\ ( W e. A /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ -. R .<_ ( ( P .\/ Q ) .\/ S ) ) ) /\ ( S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( S .\/ R ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
58 39 41 52 56 57 syl31anc 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( S .\/ R ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
59 38 58 eqtr3d 
 |-  ( ( ( ( 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 ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ W ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
60 59 3exp 
 |-  ( ( ( 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 ) ) ) -> ( -. S .<_ ( ( P .\/ Q ) .\/ W ) -> ( ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) )
61 simp1 
 |-  ( ( ( 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 ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
62 simp3 
 |-  ( ( ( 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 ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
63 1 2 3 4atlem3b 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ W e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. R .<_ ( ( P .\/ Q ) .\/ W ) \/ -. S .<_ ( ( P .\/ Q ) .\/ W ) ) )
64 61 6 10 16 62 63 syl131anc 
 |-  ( ( ( 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 ) ) ) -> ( -. R .<_ ( ( P .\/ Q ) .\/ W ) \/ -. S .<_ ( ( P .\/ Q ) .\/ W ) ) )
65 34 60 64 mpjaod 
 |-  ( ( ( 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 ) ) ) -> ( ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )
66 22 65 sylbird 
 |-  ( ( ( 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 ) ) ) -> ( ( R .\/ S ) .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )