Metamath Proof Explorer

Theorem cdleme20zN

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme20z.l 
|- .<_ = ( le ` K )
cdleme20z.j 
|- .\/ = ( join ` K )
cdleme20z.m 
|- ./\ = ( meet ` K )
cdleme20z.a 
|- A = ( Atoms ` K )
Assertion cdleme20zN 
|- ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> ( ( S .\/ R ) ./\ T ) = ( 0. ` K ) )

Proof

Step Hyp Ref Expression
1 cdleme20z.l 
 |-  .<_ = ( le ` K )
2 cdleme20z.j 
 |-  .\/ = ( join ` K )
3 cdleme20z.m 
 |-  ./\ = ( meet ` K )
4 cdleme20z.a 
 |-  A = ( Atoms ` K )
5 hllat 
 |-  ( K e. HL -> K e. Lat )
6 5 3ad2ant1 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> K e. Lat )
7 simp1 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> K e. HL )
8 simp22 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> S e. A )
9 simp21 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> R e. A )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 10 2 4 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ R e. A ) -> ( S .\/ R ) e. ( Base ` K ) )
12 7 8 9 11 syl3anc 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> ( S .\/ R ) e. ( Base ` K ) )
13 simp23 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> T e. A )
14 10 4 atbase 
 |-  ( T e. A -> T e. ( Base ` K ) )
15 13 14 syl 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> T e. ( Base ` K ) )
16 10 3 latmcom 
 |-  ( ( K e. Lat /\ ( S .\/ R ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> ( ( S .\/ R ) ./\ T ) = ( T ./\ ( S .\/ R ) ) )
17 6 12 15 16 syl3anc 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> ( ( S .\/ R ) ./\ T ) = ( T ./\ ( S .\/ R ) ) )
18 simp3r 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> -. R .<_ ( S .\/ T ) )
19 hlcvl 
 |-  ( K e. HL -> K e. CvLat )
20 19 3ad2ant1 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> K e. CvLat )
21 simp3l 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> S =/= T )
22 21 necomd 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> T =/= S )
23 1 2 4 cvlatexch1 
 |-  ( ( K e. CvLat /\ ( T e. A /\ R e. A /\ S e. A ) /\ T =/= S ) -> ( T .<_ ( S .\/ R ) -> R .<_ ( S .\/ T ) ) )
24 20 13 9 8 22 23 syl131anc 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> ( T .<_ ( S .\/ R ) -> R .<_ ( S .\/ T ) ) )
25 18 24 mtod 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> -. T .<_ ( S .\/ R ) )
26 hlatl 
 |-  ( K e. HL -> K e. AtLat )
27 26 3ad2ant1 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> K e. AtLat )
28 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
29 10 1 3 28 4 atnle 
 |-  ( ( K e. AtLat /\ T e. A /\ ( S .\/ R ) e. ( Base ` K ) ) -> ( -. T .<_ ( S .\/ R ) <-> ( T ./\ ( S .\/ R ) ) = ( 0. ` K ) ) )
30 27 13 12 29 syl3anc 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> ( -. T .<_ ( S .\/ R ) <-> ( T ./\ ( S .\/ R ) ) = ( 0. ` K ) ) )
31 25 30 mpbid 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> ( T ./\ ( S .\/ R ) ) = ( 0. ` K ) )
32 17 31 eqtrd 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( S =/= T /\ -. R .<_ ( S .\/ T ) ) ) -> ( ( S .\/ R ) ./\ T ) = ( 0. ` K ) )