Metamath Proof Explorer

Theorem cdlemednpq

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. D represents s_2. (Contributed by NM, 18-Nov-2012)

Ref Expression
Hypotheses cdlemeda.l 
|- .<_ = ( le ` K )
cdlemeda.j 
|- .\/ = ( join ` K )
cdlemeda.m 
|- ./\ = ( meet ` K )
cdlemeda.a 
|- A = ( Atoms ` K )
cdlemeda.h 
|- H = ( LHyp ` K )
cdlemeda.d 
|- D = ( ( R .\/ S ) ./\ W )
Assertion cdlemednpq 
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. D .<_ ( P .\/ Q ) )

Proof

Step Hyp Ref Expression
1 cdlemeda.l 
 |-  .<_ = ( le ` K )
2 cdlemeda.j 
 |-  .\/ = ( join ` K )
3 cdlemeda.m 
 |-  ./\ = ( meet ` K )
4 cdlemeda.a 
 |-  A = ( Atoms ` K )
5 cdlemeda.h 
 |-  H = ( LHyp ` K )
6 cdlemeda.d 
 |-  D = ( ( R .\/ S ) ./\ W )
7 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. HL )
8 7 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. Lat )
9 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> R e. A )
10 simp31l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> S e. A )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 11 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
13 7 9 10 12 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R .\/ S ) e. ( Base ` K ) )
14 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> W e. H )
15 11 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
16 14 15 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> W e. ( Base ` K ) )
17 11 1 3 latmle2 
 |-  ( ( K e. Lat /\ ( R .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( R .\/ S ) ./\ W ) .<_ W )
18 8 13 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) .<_ W )
19 6 18 eqbrtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> D .<_ W )
20 simp23r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. R .<_ W )
21 nbrne2 
 |-  ( ( D .<_ W /\ -. R .<_ W ) -> D =/= R )
22 19 20 21 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> D =/= R )
23 8 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> K e. Lat )
24 13 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> ( R .\/ S ) e. ( Base ` K ) )
25 16 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> W e. ( Base ` K ) )
26 11 1 3 latmle1 
 |-  ( ( K e. Lat /\ ( R .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( R .\/ S ) ./\ W ) .<_ ( R .\/ S ) )
27 23 24 25 26 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> ( ( R .\/ S ) ./\ W ) .<_ ( R .\/ S ) )
28 6 27 eqbrtrid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> D .<_ ( R .\/ S ) )
29 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> D .<_ ( P .\/ Q ) )
30 simp31r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. S .<_ W )
31 simp32 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> R .<_ ( P .\/ Q ) )
32 simp33 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. S .<_ ( P .\/ Q ) )
33 1 2 3 4 5 6 cdlemeda 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( R e. A /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> D e. A )
34 7 14 10 30 9 31 32 33 syl223anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> D e. A )
35 11 4 atbase 
 |-  ( D e. A -> D e. ( Base ` K ) )
36 34 35 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> D e. ( Base ` K ) )
37 36 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> D e. ( Base ` K ) )
38 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> P e. A )
39 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> Q e. A )
40 11 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
41 7 38 39 40 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
42 41 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
43 11 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( D e. ( Base ` K ) /\ ( R .\/ S ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( D .<_ ( R .\/ S ) /\ D .<_ ( P .\/ Q ) ) <-> D .<_ ( ( R .\/ S ) ./\ ( P .\/ Q ) ) ) )
44 23 37 24 42 43 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> ( ( D .<_ ( R .\/ S ) /\ D .<_ ( P .\/ Q ) ) <-> D .<_ ( ( R .\/ S ) ./\ ( P .\/ Q ) ) ) )
45 28 29 44 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> D .<_ ( ( R .\/ S ) ./\ ( P .\/ Q ) ) )
46 hlatl 
 |-  ( K e. HL -> K e. AtLat )
47 7 46 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. AtLat )
48 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
49 11 1 3 48 4 atnle 
 |-  ( ( K e. AtLat /\ S e. A /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( -. S .<_ ( P .\/ Q ) <-> ( S ./\ ( P .\/ Q ) ) = ( 0. ` K ) ) )
50 47 10 41 49 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( -. S .<_ ( P .\/ Q ) <-> ( S ./\ ( P .\/ Q ) ) = ( 0. ` K ) ) )
51 32 50 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( S ./\ ( P .\/ Q ) ) = ( 0. ` K ) )
52 51 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( S ./\ ( P .\/ Q ) ) ) = ( R .\/ ( 0. ` K ) ) )
53 11 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
54 10 53 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> S e. ( Base ` K ) )
55 11 1 2 3 4 atmod1i1 
 |-  ( ( K e. HL /\ ( R e. A /\ S e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) /\ R .<_ ( P .\/ Q ) ) -> ( R .\/ ( S ./\ ( P .\/ Q ) ) ) = ( ( R .\/ S ) ./\ ( P .\/ Q ) ) )
56 7 9 54 41 31 55 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( S ./\ ( P .\/ Q ) ) ) = ( ( R .\/ S ) ./\ ( P .\/ Q ) ) )
57 hlol 
 |-  ( K e. HL -> K e. OL )
58 7 57 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. OL )
59 11 4 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
60 9 59 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> R e. ( Base ` K ) )
61 11 2 48 olj01 
 |-  ( ( K e. OL /\ R e. ( Base ` K ) ) -> ( R .\/ ( 0. ` K ) ) = R )
62 58 60 61 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R .\/ ( 0. ` K ) ) = R )
63 52 56 62 3eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ ( P .\/ Q ) ) = R )
64 63 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> ( ( R .\/ S ) ./\ ( P .\/ Q ) ) = R )
65 45 64 breqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) /\ D .<_ ( P .\/ Q ) ) -> D .<_ R )
66 65 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( D .<_ ( P .\/ Q ) -> D .<_ R ) )
67 1 4 atcmp 
 |-  ( ( K e. AtLat /\ D e. A /\ R e. A ) -> ( D .<_ R <-> D = R ) )
68 47 34 9 67 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( D .<_ R <-> D = R ) )
69 66 68 sylibd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( D .<_ ( P .\/ Q ) -> D = R ) )
70 69 necon3ad 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( D =/= R -> -. D .<_ ( P .\/ Q ) ) )
71 22 70 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. D .<_ ( P .\/ Q ) )