Metamath Proof Explorer

Theorem cdlemb

Description: Given two atoms not less than or equal to an element covered by 1, there is a third. Lemma B in Crawley p. 112. (Contributed by NM, 8-May-2012)

Ref Expression
Hypotheses cdlemb.b 
|- B = ( Base ` K )
cdlemb.l 
|- .<_ = ( le ` K )
cdlemb.j 
|- .\/ = ( join ` K )
cdlemb.u 
|- .1. = ( 1. ` K )
cdlemb.c 
|- C = (
cdlemb.a 
|- A = ( Atoms ` K )
Assertion cdlemb 
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> E. r e. A ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) )

Proof

Step Hyp Ref Expression
1 cdlemb.b 
 |-  B = ( Base ` K )
2 cdlemb.l 
 |-  .<_ = ( le ` K )
3 cdlemb.j 
 |-  .\/ = ( join ` K )
4 cdlemb.u 
 |-  .1. = ( 1. ` K )
5 cdlemb.c 
 |-  C = (
6 cdlemb.a 
 |-  A = ( Atoms ` K )
7 simp11 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> K e. HL )
8 simp12 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> P e. A )
9 simp13 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> Q e. A )
10 simp2l 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> X e. B )
11 simp2r 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> P =/= Q )
12 simp31 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> X C .1. )
13 simp32 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> -. P .<_ X )
14 eqid 
 |-  ( meet ` K ) = ( meet ` K )
15 1 2 3 14 4 5 6 1cvrat 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P =/= Q /\ X C .1. /\ -. P .<_ X ) ) -> ( ( P .\/ Q ) ( meet ` K ) X ) e. A )
16 7 8 9 10 11 12 13 15 syl133anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> ( ( P .\/ Q ) ( meet ` K ) X ) e. A )
17 7 hllatd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> K e. Lat )
18 1 6 atbase 
 |-  ( P e. A -> P e. B )
19 8 18 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> P e. B )
20 1 6 atbase 
 |-  ( Q e. A -> Q e. B )
21 9 20 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> Q e. B )
22 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) e. B )
23 17 19 21 22 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> ( P .\/ Q ) e. B )
24 1 2 14 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. B /\ X e. B ) -> ( ( P .\/ Q ) ( meet ` K ) X ) .<_ X )
25 17 23 10 24 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> ( ( P .\/ Q ) ( meet ` K ) X ) .<_ X )
26 eqid 
 |-  ( lt ` K ) = ( lt ` K )
27 1 2 26 4 5 6 1cvratlt 
 |-  ( ( ( K e. HL /\ ( ( P .\/ Q ) ( meet ` K ) X ) e. A /\ X e. B ) /\ ( X C .1. /\ ( ( P .\/ Q ) ( meet ` K ) X ) .<_ X ) ) -> ( ( P .\/ Q ) ( meet ` K ) X ) ( lt ` K ) X )
28 7 16 10 12 25 27 syl32anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> ( ( P .\/ Q ) ( meet ` K ) X ) ( lt ` K ) X )
29 1 26 6 2atlt 
 |-  ( ( ( K e. HL /\ ( ( P .\/ Q ) ( meet ` K ) X ) e. A /\ X e. B ) /\ ( ( P .\/ Q ) ( meet ` K ) X ) ( lt ` K ) X ) -> E. u e. A ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) )
30 7 16 10 28 29 syl31anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> E. u e. A ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) )
31 simpl11 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> K e. HL )
32 simpl12 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> P e. A )
33 simprl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> u e. A )
34 simpl32 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> -. P .<_ X )
35 simprrr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> u ( lt ` K ) X )
36 simpl2l 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> X e. B )
37 2 26 pltle 
 |-  ( ( K e. HL /\ u e. A /\ X e. B ) -> ( u ( lt ` K ) X -> u .<_ X ) )
38 31 33 36 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> ( u ( lt ` K ) X -> u .<_ X ) )
39 35 38 mpd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> u .<_ X )
40 breq1 
 |-  ( P = u -> ( P .<_ X <-> u .<_ X ) )
41 39 40 syl5ibrcom 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> ( P = u -> P .<_ X ) )
42 41 necon3bd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> ( -. P .<_ X -> P =/= u ) )
43 34 42 mpd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> P =/= u )
44 2 3 6 hlsupr 
 |-  ( ( ( K e. HL /\ P e. A /\ u e. A ) /\ P =/= u ) -> E. r e. A ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) )
45 31 32 33 43 44 syl31anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> E. r e. A ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) )
46 eqid 
 |-  ( ( P .\/ Q ) ( meet ` K ) X ) = ( ( P .\/ Q ) ( meet ` K ) X )
47 1 2 3 4 5 6 26 14 46 cdlemblem 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) /\ ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) ) -> ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) )
48 47 3exp 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> ( ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) -> ( ( r e. A /\ ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) ) -> ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) ) ) )
49 48 exp4a 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> ( ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) -> ( r e. A -> ( ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) -> ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) ) ) ) )
50 49 imp 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> ( r e. A -> ( ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) -> ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) ) ) )
51 50 reximdvai 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> ( E. r e. A ( r =/= P /\ r =/= u /\ r .<_ ( P .\/ u ) ) -> E. r e. A ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) ) )
52 45 51 mpd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) /\ ( u e. A /\ ( u =/= ( ( P .\/ Q ) ( meet ` K ) X ) /\ u ( lt ` K ) X ) ) ) -> E. r e. A ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) )
53 30 52 rexlimddv 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( X e. B /\ P =/= Q ) /\ ( X C .1. /\ -. P .<_ X /\ -. Q .<_ X ) ) -> E. r e. A ( -. r .<_ X /\ -. r .<_ ( P .\/ Q ) ) )