Metamath Proof Explorer

Theorem 4atlem12b

Description: Lemma for 4at . Substitute T for P (cont.). (Contributed by NM, 11-Jul-2012)

Ref Expression
Hypotheses 4at.l 
|- .<_ = ( le ` K )
4at.j 
|- .\/ = ( join ` K )
4at.a 
|- A = ( Atoms ` K )
Assertion 4atlem12b 
|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ 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 simp11 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
5 simp121 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> R e. A )
6 simp122 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> S e. A )
7 5 6 jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( R e. A /\ S e. A ) )
8 simp13 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( U e. A /\ V e. A /\ W e. A ) )
9 4 7 8 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ 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 ) ) )
10 simp2l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
11 9 10 jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ 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 ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) )
12 simp3lr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
13 simp3rl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
14 simp3rr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
15 simp111 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> K e. HL )
16 15 hllatd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> K e. Lat )
17 eqid 
 |-  ( Base ` K ) = ( Base ` K )
18 17 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
19 5 18 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> R e. ( Base ` K ) )
20 17 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
21 6 20 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> S e. ( Base ` K ) )
22 simp123 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> T e. A )
23 simp131 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> U e. A )
24 17 2 3 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
25 15 22 23 24 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( T .\/ U ) e. ( Base ` K ) )
26 simp132 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> V e. A )
27 simp133 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> W e. A )
28 17 2 3 hlatjcl 
 |-  ( ( K e. HL /\ V e. A /\ W e. A ) -> ( V .\/ W ) e. ( Base ` K ) )
29 15 26 27 28 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( V .\/ W ) e. ( Base ` K ) )
30 17 2 latjcl 
 |-  ( ( K e. Lat /\ ( T .\/ U ) e. ( Base ` K ) /\ ( V .\/ W ) e. ( Base ` K ) ) -> ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) )
31 16 25 29 30 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) )
32 17 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ S e. ( Base ` K ) /\ ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) ) ) -> ( ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
33 16 19 21 31 32 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
34 13 14 33 mpbi2and 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
35 simp113 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> Q e. A )
36 17 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
37 35 36 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> Q e. ( Base ` K ) )
38 17 2 3 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
39 15 5 6 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( R .\/ S ) e. ( Base ` K ) )
40 17 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ ( R .\/ S ) e. ( Base ` K ) /\ ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) ) ) -> ( ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( Q .\/ ( R .\/ S ) ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
41 16 37 39 31 40 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( Q .\/ ( R .\/ S ) ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
42 12 34 41 mpbi2and 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( Q .\/ ( R .\/ S ) ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
43 simp3ll 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
44 simp112 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> P e. A )
45 simp2r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> -. P .<_ ( ( U .\/ V ) .\/ W ) )
46 1 2 3 4atlem12a 
 |-  ( ( ( K e. HL /\ P e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) -> ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) <-> ( ( P .\/ U ) .\/ ( V .\/ W ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
47 15 44 22 8 45 46 syl311anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) <-> ( ( P .\/ U ) .\/ ( V .\/ W ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
48 43 47 mpbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ U ) .\/ ( V .\/ W ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
49 42 48 breqtrrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( Q .\/ ( R .\/ S ) ) .<_ ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
50 1 2 3 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 ) ) ) )
51 11 49 50 sylc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ U ) .\/ ( V .\/ W ) ) )
52 51 48 eqtrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )