Metamath Proof Explorer

Theorem dalawlem15

Description: Lemma for dalaw . Swap variable triples P Q R and S T U in dalawlem14 , to obtain the elimination of the remaining conditions in dalawlem1 . (Contributed by NM, 6-Oct-2012)

Ref Expression
Hypotheses dalawlem.l 
|- .<_ = ( le ` K )
dalawlem.j 
|- .\/ = ( join ` K )
dalawlem.m 
|- ./\ = ( meet ` K )
dalawlem.a 
|- A = ( Atoms ` K )
dalawlem2.o 
|- O = ( LPlanes ` K )
Assertion dalawlem15 
|- ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 dalawlem2.o 
 |-  O = ( LPlanes ` K )
6 simp11 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 simp12 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) )
8 simp21 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 simp31 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 )
10 2 4 hlatjcom 
 |-  ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) = ( S .\/ P ) )
11 6 8 9 10 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 .\/ P ) )
12 simp22 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 )
13 simp32 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 2 4 hlatjcom 
 |-  ( ( K e. HL /\ Q e. A /\ T e. A ) -> ( Q .\/ T ) = ( T .\/ Q ) )
15 6 12 13 14 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) = ( T .\/ Q ) )
16 11 15 oveq12d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) = ( ( S .\/ P ) ./\ ( T .\/ Q ) ) )
17 16 breq1d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) .<_ ( S .\/ T ) <-> ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( S .\/ T ) ) )
18 17 notbid 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) .<_ ( S .\/ T ) <-> -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( S .\/ T ) ) )
19 16 breq1d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) .<_ ( T .\/ U ) <-> ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( T .\/ U ) ) )
20 19 notbid 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) .<_ ( T .\/ U ) <-> -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( T .\/ U ) ) )
21 16 breq1d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) .<_ ( U .\/ S ) <-> ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( U .\/ S ) ) )
22 21 notbid 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) .<_ ( U .\/ S ) <-> -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( U .\/ S ) ) )
23 18 20 22 3anbi123d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) <-> ( -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( S .\/ T ) /\ -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( T .\/ U ) /\ -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( U .\/ S ) ) ) )
24 23 anbi2d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) <-> ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( S .\/ T ) /\ -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( T .\/ U ) /\ -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( U .\/ S ) ) ) ) )
25 7 24 mtbid 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) .\/ U ) e. O /\ ( -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( S .\/ T ) /\ -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( T .\/ U ) /\ -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( U .\/ S ) ) ) )
26 simp13 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) )
27 2 4 hlatjcom 
 |-  ( ( K e. HL /\ S e. A /\ P e. A ) -> ( S .\/ P ) = ( P .\/ S ) )
28 6 9 8 27 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) = ( P .\/ S ) )
29 2 4 hlatjcom 
 |-  ( ( K e. HL /\ T e. A /\ Q e. A ) -> ( T .\/ Q ) = ( Q .\/ T ) )
30 6 13 12 29 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 .\/ Q ) = ( Q .\/ T ) )
31 28 30 oveq12d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ./\ ( T .\/ Q ) ) = ( ( P .\/ S ) ./\ ( Q .\/ T ) ) )
32 simp33 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 )
33 simp23 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 )
34 2 4 hlatjcom 
 |-  ( ( K e. HL /\ U e. A /\ R e. A ) -> ( U .\/ R ) = ( R .\/ U ) )
35 6 32 33 34 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 .\/ R ) = ( R .\/ U ) )
36 26 31 35 3brtr4d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ./\ ( T .\/ Q ) ) .<_ ( U .\/ R ) )
37 simp3 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 /\ T e. A /\ U e. A ) )
38 simp2 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 /\ Q e. A /\ R e. A ) )
39 1 2 3 4 5 dalawlem14 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( S .\/ T ) /\ -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( T .\/ U ) /\ -. ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( U .\/ S ) ) ) /\ ( ( S .\/ P ) ./\ ( T .\/ Q ) ) .<_ ( U .\/ R ) ) /\ ( S e. A /\ T e. A /\ U e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( S .\/ T ) ./\ ( P .\/ Q ) ) .<_ ( ( ( T .\/ U ) ./\ ( Q .\/ R ) ) .\/ ( ( U .\/ S ) ./\ ( R .\/ P ) ) ) )
40 6 25 36 37 38 39 syl311anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ./\ ( P .\/ Q ) ) .<_ ( ( ( T .\/ U ) ./\ ( Q .\/ R ) ) .\/ ( ( U .\/ S ) ./\ ( R .\/ P ) ) ) )
41 6 hllatd 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 )
42 eqid 
 |-  ( Base ` K ) = ( Base ` K )
43 42 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
44 6 8 12 43 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) )
45 42 2 4 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
46 6 9 13 45 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) )
47 42 3 latmcom 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) = ( ( S .\/ T ) ./\ ( P .\/ Q ) ) )
48 41 44 46 47 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) = ( ( S .\/ T ) ./\ ( P .\/ Q ) ) )
49 42 2 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
50 6 12 33 49 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) )
51 42 2 4 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
52 6 13 32 51 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) )
53 42 3 latmcom 
 |-  ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) /\ ( T .\/ U ) e. ( Base ` K ) ) -> ( ( Q .\/ R ) ./\ ( T .\/ U ) ) = ( ( T .\/ U ) ./\ ( Q .\/ R ) ) )
54 41 50 52 53 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) = ( ( T .\/ U ) ./\ ( Q .\/ R ) ) )
55 42 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ P e. A ) -> ( R .\/ P ) e. ( Base ` K ) )
56 6 33 8 55 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) )
57 42 2 4 hlatjcl 
 |-  ( ( K e. HL /\ U e. A /\ S e. A ) -> ( U .\/ S ) e. ( Base ` K ) )
58 6 32 9 57 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) )
59 42 3 latmcom 
 |-  ( ( K e. Lat /\ ( R .\/ P ) e. ( Base ` K ) /\ ( U .\/ S ) e. ( Base ` K ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) = ( ( U .\/ S ) ./\ ( R .\/ P ) ) )
60 41 56 58 59 syl3anc 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 .\/ S ) ./\ ( R .\/ P ) ) )
61 54 60 oveq12d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) ) = ( ( ( T .\/ U ) ./\ ( Q .\/ R ) ) .\/ ( ( U .\/ S ) ./\ ( R .\/ P ) ) ) )
62 40 48 61 3brtr4d 
 |-  ( ( ( K e. HL /\ -. ( ( ( S .\/ T ) .\/ U ) e. O /\ ( -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( S .\/ T ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( T .\/ U ) /\ -. ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ S ) ) ) /\ ( ( 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 ) ) ) )