Metamath Proof Explorer

Theorem dalawlem4

Description: Lemma for dalaw . Second piece of dalawlem5 . (Contributed by NM, 4-Oct-2012)

Ref Expression
Hypotheses dalawlem.l 
|- .<_ = ( le ` K )
dalawlem.j 
|- .\/ = ( join ` K )
dalawlem.m 
|- ./\ = ( meet ` K )
dalawlem.a 
|- A = ( Atoms ` K )
Assertion dalawlem4 
|- ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) .<_ ( ( ( 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 simp11 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 )
6 simp12 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) ) .<_ ( P .\/ Q ) )
7 5 hllatd 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. Lat )
8 simp22 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 )
9 simp32 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ T e. A ) -> ( Q .\/ T ) e. ( Base ` K ) )
12 5 8 9 11 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ T ) e. ( Base ` K ) )
13 simp21 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 )
14 simp31 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 )
15 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) e. ( Base ` K ) )
16 5 13 14 15 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ S ) e. ( Base ` K ) )
17 10 3 latmcom 
 |-  ( ( K e. Lat /\ ( Q .\/ T ) e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) = ( ( P .\/ S ) ./\ ( Q .\/ T ) ) )
18 7 12 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) = ( ( P .\/ S ) ./\ ( Q .\/ T ) ) )
19 2 4 hlatjcom 
 |-  ( ( K e. HL /\ Q e. A /\ P e. A ) -> ( Q .\/ P ) = ( P .\/ Q ) )
20 5 8 13 19 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 .\/ P ) = ( P .\/ Q ) )
21 6 18 20 3brtr4d 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) .<_ ( Q .\/ P ) )
22 simp13 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) )
23 18 22 eqbrtrd 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ T ) ./\ ( P .\/ S ) ) .<_ ( R .\/ U ) )
24 simp23 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 )
25 simp33 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 )
26 1 2 3 4 dalawlem3 
 |-  ( ( ( K e. HL /\ ( ( Q .\/ T ) ./\ ( P .\/ S ) ) .<_ ( Q .\/ P ) /\ ( ( Q .\/ T ) ./\ ( P .\/ S ) ) .<_ ( R .\/ U ) ) /\ ( Q e. A /\ P e. A /\ R e. A ) /\ ( T e. A /\ S e. A /\ U e. A ) ) -> ( ( ( P .\/ S ) .\/ Q ) ./\ T ) .<_ ( ( ( P .\/ R ) ./\ ( S .\/ U ) ) .\/ ( ( R .\/ Q ) ./\ ( U .\/ T ) ) ) )
27 5 21 23 8 13 24 9 14 25 26 syl333anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) .<_ ( ( ( P .\/ R ) ./\ ( S .\/ U ) ) .\/ ( ( R .\/ Q ) ./\ ( U .\/ T ) ) ) )
28 2 4 hlatjcom 
 |-  ( ( K e. HL /\ P e. A /\ R e. A ) -> ( P .\/ R ) = ( R .\/ P ) )
29 5 13 24 28 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ R ) = ( R .\/ P ) )
30 2 4 hlatjcom 
 |-  ( ( K e. HL /\ S e. A /\ U e. A ) -> ( S .\/ U ) = ( U .\/ S ) )
31 5 14 25 30 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( S .\/ U ) = ( U .\/ S ) )
32 29 31 oveq12d 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ R ) ./\ ( S .\/ U ) ) = ( ( R .\/ P ) ./\ ( U .\/ S ) ) )
33 2 4 hlatjcom 
 |-  ( ( K e. HL /\ R e. A /\ Q e. A ) -> ( R .\/ Q ) = ( Q .\/ R ) )
34 5 24 8 33 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( R .\/ Q ) = ( Q .\/ R ) )
35 2 4 hlatjcom 
 |-  ( ( K e. HL /\ U e. A /\ T e. A ) -> ( U .\/ T ) = ( T .\/ U ) )
36 5 25 9 35 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 .\/ T ) = ( T .\/ U ) )
37 34 36 oveq12d 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( R .\/ Q ) ./\ ( U .\/ T ) ) = ( ( Q .\/ R ) ./\ ( T .\/ U ) ) )
38 32 37 oveq12d 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ R ) ./\ ( S .\/ U ) ) .\/ ( ( R .\/ Q ) ./\ ( U .\/ T ) ) ) = ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ ( ( Q .\/ R ) ./\ ( T .\/ U ) ) ) )
39 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ P e. A ) -> ( R .\/ P ) e. ( Base ` K ) )
40 5 24 13 39 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) )
41 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ U e. A /\ S e. A ) -> ( U .\/ S ) e. ( Base ` K ) )
42 5 25 14 41 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) )
43 10 3 latmcl 
 |-  ( ( K e. Lat /\ ( R .\/ P ) e. ( Base ` K ) /\ ( U .\/ S ) e. ( Base ` K ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) )
44 7 40 42 43 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) )
45 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
46 5 8 24 45 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) )
47 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
48 5 9 25 47 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) )
49 10 3 latmcl 
 |-  ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) /\ ( T .\/ U ) e. ( Base ` K ) ) -> ( ( Q .\/ R ) ./\ ( T .\/ U ) ) e. ( Base ` K ) )
50 7 46 48 49 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) ) e. ( Base ` K ) )
51 10 2 latjcom 
 |-  ( ( K e. Lat /\ ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) /\ ( ( Q .\/ R ) ./\ ( T .\/ U ) ) e. ( Base ` K ) ) -> ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ ( ( Q .\/ R ) ./\ ( T .\/ U ) ) ) = ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
52 7 44 50 51 syl3anc 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( R .\/ P ) ./\ ( U .\/ S ) ) .\/ ( ( Q .\/ R ) ./\ ( T .\/ U ) ) ) = ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
53 38 52 eqtrd 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ R ) ./\ ( S .\/ U ) ) .\/ ( ( R .\/ Q ) ./\ ( U .\/ T ) ) ) = ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
54 27 53 breqtrd 
 |-  ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( 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 ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )