Metamath Proof Explorer

Theorem 3dimlem3OLDN

Description: Lemma for 3dim1 . (Contributed by NM, 25-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses 3dim0.j 
|- .\/ = ( join ` K )
3dim0.l 
|- .<_ = ( le ` K )
3dim0.a 
|- A = ( Atoms ` K )
Assertion 3dimlem3OLDN 
|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) )

Proof

Step Hyp Ref Expression
1 3dim0.j 
 |-  .\/ = ( join ` K )
2 3dim0.l 
 |-  .<_ = ( le ` K )
3 3dim0.a 
 |-  A = ( Atoms ` K )
4 simpr1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> P =/= Q )
5 simpr2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> -. P .<_ ( Q .\/ R ) )
6 simpl11 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> K e. HL )
7 simpl2l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> R e. A )
8 simpl12 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> P e. A )
9 simpl13 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> Q e. A )
10 simpl3l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> Q =/= R )
11 10 necomd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> R =/= Q )
12 2 1 3 hlatexch2 
 |-  ( ( K e. HL /\ ( R e. A /\ P e. A /\ Q e. A ) /\ R =/= Q ) -> ( R .<_ ( P .\/ Q ) -> P .<_ ( R .\/ Q ) ) )
13 6 7 8 9 11 12 syl131anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( R .<_ ( P .\/ Q ) -> P .<_ ( R .\/ Q ) ) )
14 1 3 hlatjcom 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) = ( R .\/ Q ) )
15 6 9 7 14 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( Q .\/ R ) = ( R .\/ Q ) )
16 15 breq2d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( P .<_ ( Q .\/ R ) <-> P .<_ ( R .\/ Q ) ) )
17 13 16 sylibrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( R .<_ ( P .\/ Q ) -> P .<_ ( Q .\/ R ) ) )
18 5 17 mtod 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> -. R .<_ ( P .\/ Q ) )
19 simpl3r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> -. T .<_ ( ( Q .\/ R ) .\/ S ) )
20 hllat 
 |-  ( K e. HL -> K e. Lat )
21 6 20 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> K e. Lat )
22 eqid 
 |-  ( Base ` K ) = ( Base ` K )
23 22 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
24 9 23 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> Q e. ( Base ` K ) )
25 22 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
26 7 25 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> R e. ( Base ` K ) )
27 22 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
28 8 27 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> P e. ( Base ` K ) )
29 22 1 latjrot 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ R e. ( Base ` K ) /\ P e. ( Base ` K ) ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) )
30 21 24 26 28 29 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) )
31 simpr3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> P .<_ ( ( Q .\/ R ) .\/ S ) )
32 simpl2r 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> S e. A )
33 22 1 3 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
34 6 9 7 33 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
35 22 2 1 3 hlexchb1 
 |-  ( ( K e. HL /\ ( P e. A /\ S e. A /\ ( Q .\/ R ) e. ( Base ` K ) ) /\ -. P .<_ ( Q .\/ R ) ) -> ( P .<_ ( ( Q .\/ R ) .\/ S ) <-> ( ( Q .\/ R ) .\/ P ) = ( ( Q .\/ R ) .\/ S ) ) )
36 6 8 32 34 5 35 syl131anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( P .<_ ( ( Q .\/ R ) .\/ S ) <-> ( ( Q .\/ R ) .\/ P ) = ( ( Q .\/ R ) .\/ S ) ) )
37 31 36 mpbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( Q .\/ R ) .\/ S ) )
38 30 37 eqtr3d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( Q .\/ R ) .\/ S ) )
39 38 breq2d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( T .<_ ( ( P .\/ Q ) .\/ R ) <-> T .<_ ( ( Q .\/ R ) .\/ S ) ) )
40 19 39 mtbird 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> -. T .<_ ( ( P .\/ Q ) .\/ R ) )
41 4 18 40 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( Q =/= R /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) /\ ( P =/= Q /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) )