Metamath Proof Explorer

Theorem 3dimlem3a

Description: Lemma for 3dim3 . (Contributed by NM, 27-Jul-2012)

Ref Expression
Hypotheses 3dim0.j 
|- .\/ = ( join ` K )
3dim0.l 
|- .<_ = ( le ` K )
3dim0.a 
|- A = ( Atoms ` K )
Assertion 3dimlem3a 
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> -. 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 simp31 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> -. T .<_ ( ( Q .\/ R ) .\/ S ) )
5 simp11 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> K e. HL )
6 5 hllatd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> K e. Lat )
7 simp13 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> Q e. A )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 8 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
10 7 9 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> Q e. ( Base ` K ) )
11 simp2l 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> R e. A )
12 8 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
13 11 12 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> R e. ( Base ` K ) )
14 simp12 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> P e. A )
15 8 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
16 14 15 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> P e. ( Base ` K ) )
17 8 1 latjrot 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ R e. ( Base ` K ) /\ P e. ( Base ` K ) ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) )
18 6 10 13 16 17 syl13anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) )
19 simp33 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> P .<_ ( ( Q .\/ R ) .\/ S ) )
20 simp2r 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> S e. A )
21 8 1 3 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
22 5 7 11 21 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
23 simp32 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> -. P .<_ ( Q .\/ R ) )
24 8 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 ) ) )
25 5 14 20 22 23 24 syl131anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( P .<_ ( ( Q .\/ R ) .\/ S ) <-> ( ( Q .\/ R ) .\/ P ) = ( ( Q .\/ R ) .\/ S ) ) )
26 19 25 mpbid 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( ( Q .\/ R ) .\/ P ) = ( ( Q .\/ R ) .\/ S ) )
27 18 26 eqtr3d 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( Q .\/ R ) .\/ S ) )
28 27 breq2d 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> ( T .<_ ( ( P .\/ Q ) .\/ R ) <-> T .<_ ( ( Q .\/ R ) .\/ S ) ) )
29 4 28 mtbird 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( -. T .<_ ( ( Q .\/ R ) .\/ S ) /\ -. P .<_ ( Q .\/ R ) /\ P .<_ ( ( Q .\/ R ) .\/ S ) ) ) -> -. T .<_ ( ( P .\/ Q ) .\/ R ) )