Metamath Proof Explorer

Theorem cdleme3

Description: Part of proof of Lemma E in Crawley p. 113. F represents f(r). W is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa above, we show that f(r) e. W (4th line from bottom on p. 113), meaning it is an atom and not under w, which in our notation is expressed as F e. A /\ -. F .<_ W . Their proof provides no details of our lemmas cdleme3b through cdleme3 , so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012)

Ref Expression
Hypotheses cdleme1.l 
|- .<_ = ( le ` K )
cdleme1.j 
|- .\/ = ( join ` K )
cdleme1.m 
|- ./\ = ( meet ` K )
cdleme1.a 
|- A = ( Atoms ` K )
cdleme1.h 
|- H = ( LHyp ` K )
cdleme1.u 
|- U = ( ( P .\/ Q ) ./\ W )
cdleme1.f 
|- F = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
Assertion cdleme3 
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> -. F .<_ W )

Proof

Step Hyp Ref Expression
1 cdleme1.l 
 |-  .<_ = ( le ` K )
2 cdleme1.j 
 |-  .\/ = ( join ` K )
3 cdleme1.m 
 |-  ./\ = ( meet ` K )
4 cdleme1.a 
 |-  A = ( Atoms ` K )
5 cdleme1.h 
 |-  H = ( LHyp ` K )
6 cdleme1.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
7 cdleme1.f 
 |-  F = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
8 eqid 
 |-  ( ( P .\/ R ) ./\ W ) = ( ( P .\/ R ) ./\ W )
9 1 2 3 4 5 6 7 8 cdleme3g 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> F =/= U )
10 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> K e. HL )
11 10 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> K e. Lat )
12 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> R e. A )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 13 4 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
15 12 14 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> R e. ( Base ` K ) )
16 1 2 3 4 5 6 7 cdleme3fa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> F e. A )
17 13 4 atbase 
 |-  ( F e. A -> F e. ( Base ` K ) )
18 16 17 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> F e. ( Base ` K ) )
19 13 1 2 latlej2 
 |-  ( ( K e. Lat /\ R e. ( Base ` K ) /\ F e. ( Base ` K ) ) -> F .<_ ( R .\/ F ) )
20 11 15 18 19 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> F .<_ ( R .\/ F ) )
21 20 biantrurd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( F .<_ W <-> ( F .<_ ( R .\/ F ) /\ F .<_ W ) ) )
22 13 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ F e. A ) -> ( R .\/ F ) e. ( Base ` K ) )
23 10 12 16 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( R .\/ F ) e. ( Base ` K ) )
24 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> W e. H )
25 13 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
26 24 25 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> W e. ( Base ` K ) )
27 13 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( F e. ( Base ` K ) /\ ( R .\/ F ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( F .<_ ( R .\/ F ) /\ F .<_ W ) <-> F .<_ ( ( R .\/ F ) ./\ W ) ) )
28 11 18 23 26 27 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( F .<_ ( R .\/ F ) /\ F .<_ W ) <-> F .<_ ( ( R .\/ F ) ./\ W ) ) )
29 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
30 simp21l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> P e. A )
31 simp22l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> Q e. A )
32 simp23 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( R e. A /\ -. R .<_ W ) )
33 1 2 3 4 5 6 7 cdleme2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) ) -> ( ( R .\/ F ) ./\ W ) = U )
34 29 30 31 32 33 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ F ) ./\ W ) = U )
35 34 breq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( F .<_ ( ( R .\/ F ) ./\ W ) <-> F .<_ U ) )
36 28 35 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( F .<_ ( R .\/ F ) /\ F .<_ W ) <-> F .<_ U ) )
37 hlatl 
 |-  ( K e. HL -> K e. AtLat )
38 10 37 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> K e. AtLat )
39 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( P e. A /\ -. P .<_ W ) )
40 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> P =/= Q )
41 1 2 3 4 5 6 lhpat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> U e. A )
42 29 39 31 40 41 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> U e. A )
43 1 4 atcmp 
 |-  ( ( K e. AtLat /\ F e. A /\ U e. A ) -> ( F .<_ U <-> F = U ) )
44 38 16 42 43 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( F .<_ U <-> F = U ) )
45 21 36 44 3bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( F .<_ W <-> F = U ) )
46 45 necon3bbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( -. F .<_ W <-> F =/= U ) )
47 9 46 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> -. F .<_ W )