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 ) ) )