# 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 ‘ 𝐾 )
cdlemb2.j = ( join ‘ 𝐾 )
cdlemb2.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemb2.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdlemb2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ¬ 𝑟 ( 𝑃 𝑄 ) ) )

### Proof

Step Hyp Ref Expression
1 cdlemb2.l = ( le ‘ 𝐾 )
2 cdlemb2.j = ( join ‘ 𝐾 )
3 cdlemb2.a 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemb2.h 𝐻 = ( LHyp ‘ 𝐾 )
5 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → 𝐾 ∈ HL )
6 simp2ll ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → 𝑃𝐴 )
7 simp2rl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → 𝑄𝐴 )
8 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → 𝑊𝐻 )
9 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 4 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
11 8 10 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
12 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → 𝑃𝑄 )
13 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
14 eqid ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
15 13 14 4 lhp1cvr ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
16 15 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
17 simp2lr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → ¬ 𝑃 𝑊 )
18 simp2rr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → ¬ 𝑄 𝑊 )
19 9 1 2 13 14 3 cdlemb ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃𝑄 ) ∧ ( 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ∧ ¬ 𝑃 𝑊 ∧ ¬ 𝑄 𝑊 ) ) → ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ¬ 𝑟 ( 𝑃 𝑄 ) ) )
20 5 6 7 11 12 16 17 18 19 syl323anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ¬ 𝑟 ( 𝑃 𝑄 ) ) )