This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme21b

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 28-Nov-2012)

Ref Expression
Hypotheses cdleme21a.l 
|- .<_ = ( le ` K )
cdleme21a.j 
|- .\/ = ( join ` K )
cdleme21a.a 
|- A = ( Atoms ` K )
Assertion cdleme21b 
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> -. z .<_ ( P .\/ Q ) )

Proof

Step Hyp Ref Expression
1 cdleme21a.l 
 |-  .<_ = ( le ` K )
2 cdleme21a.j 
 |-  .\/ = ( join ` K )
3 cdleme21a.a 
 |-  A = ( Atoms ` K )
4 simp23 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> -. S .<_ ( P .\/ Q ) )
5 simp11 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> K e. HL )
6 hlcvl 
 |-  ( K e. HL -> K e. CvLat )
7 5 6 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> K e. CvLat )
8 simp3l 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> z e. A )
9 simp13 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> Q e. A )
10 simp12 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> P e. A )
11 simp21 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> S e. A )
12 1 2 3 atnlej1 
 |-  ( ( K e. HL /\ ( S e. A /\ P e. A /\ Q e. A ) /\ -. S .<_ ( P .\/ Q ) ) -> S =/= P )
13 12 necomd 
 |-  ( ( K e. HL /\ ( S e. A /\ P e. A /\ Q e. A ) /\ -. S .<_ ( P .\/ Q ) ) -> P =/= S )
14 5 11 10 9 4 13 syl131anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> P =/= S )
15 simp3r 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( P .\/ z ) = ( S .\/ z ) )
16 3 2 cvlsupr5 
 |-  ( ( K e. CvLat /\ ( P e. A /\ S e. A /\ z e. A ) /\ ( P =/= S /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> z =/= P )
17 7 10 11 8 14 15 16 syl132anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> z =/= P )
18 1 2 3 cvlatexch1 
 |-  ( ( K e. CvLat /\ ( z e. A /\ Q e. A /\ P e. A ) /\ z =/= P ) -> ( z .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ z ) ) )
19 7 8 9 10 17 18 syl131anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( z .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ z ) ) )
20 3 2 cvlsupr8 
 |-  ( ( K e. CvLat /\ ( P e. A /\ S e. A /\ z e. A ) /\ ( P =/= S /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( P .\/ S ) = ( P .\/ z ) )
21 7 10 11 8 14 15 20 syl132anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( P .\/ S ) = ( P .\/ z ) )
22 21 breq2d 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( Q .<_ ( P .\/ S ) <-> Q .<_ ( P .\/ z ) ) )
23 19 22 sylibrd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( z .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ S ) ) )
24 simp22 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> P =/= Q )
25 24 necomd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> Q =/= P )
26 1 2 3 cvlatexch1 
 |-  ( ( K e. CvLat /\ ( Q e. A /\ S e. A /\ P e. A ) /\ Q =/= P ) -> ( Q .<_ ( P .\/ S ) -> S .<_ ( P .\/ Q ) ) )
27 7 9 11 10 25 26 syl131anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( Q .<_ ( P .\/ S ) -> S .<_ ( P .\/ Q ) ) )
28 23 27 syld 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( z .<_ ( P .\/ Q ) -> S .<_ ( P .\/ Q ) ) )
29 4 28 mtod 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> -. z .<_ ( P .\/ Q ) )