Metamath Proof Explorer

Theorem cdlemb2

Description: Given two atoms not under the fiducial (reference) co-atom W , there is a third. Lemma B in Crawley p. 112. (Contributed by NM, 30-May-2012)

Ref Expression
Hypotheses cdlemb2.l 
|- .<_ = ( le ` K )
cdlemb2.j 
|- .\/ = ( join ` K )
cdlemb2.a 
|- A = ( Atoms ` K )
cdlemb2.h 
|- H = ( LHyp ` K )
Assertion cdlemb2 
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) )

Proof

Step Hyp Ref Expression
1 cdlemb2.l 
 |-  .<_ = ( le ` K )
2 cdlemb2.j 
 |-  .\/ = ( join ` K )
3 cdlemb2.a 
 |-  A = ( Atoms ` K )
4 cdlemb2.h 
 |-  H = ( LHyp ` K )
5 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> K e. HL )
6 simp2ll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> P e. A )
7 simp2rl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> Q e. A )
8 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> W e. H )
9 eqid 
 |-  ( Base ` K ) = ( Base ` K )
10 9 4 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
11 8 10 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> W e. ( Base ` K ) )
12 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> P =/= Q )
13 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
14 eqid 
 |-  (
15 13 14 4 lhp1cvr 
 |-  ( ( K e. HL /\ W e. H ) -> W (
16 15 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> W (
17 simp2lr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> -. P .<_ W )
18 simp2rr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> -. Q .<_ W )
19 9 1 2 13 14 3 cdlemb 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( W e. ( Base ` K ) /\ P =/= Q ) /\ ( W (  E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) )
20 5 6 7 11 12 16 17 18 19 syl323anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) )