Metamath Proof Explorer


Theorem cdleme9a

Description: Part of proof of Lemma E in Crawley p. 113. C represents s_1, which we prove is an atom. (Contributed by NM, 10-Jun-2012)

Ref Expression
Hypotheses cdleme8.l = ( le ‘ 𝐾 )
cdleme8.j = ( join ‘ 𝐾 )
cdleme8.m = ( meet ‘ 𝐾 )
cdleme8.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme8.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme8.4 𝐶 = ( ( 𝑃 𝑆 ) 𝑊 )
Assertion cdleme9a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑆𝐴𝑃𝑆 ) ) → 𝐶𝐴 )

Proof

Step Hyp Ref Expression
1 cdleme8.l = ( le ‘ 𝐾 )
2 cdleme8.j = ( join ‘ 𝐾 )
3 cdleme8.m = ( meet ‘ 𝐾 )
4 cdleme8.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme8.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme8.4 𝐶 = ( ( 𝑃 𝑆 ) 𝑊 )
7 1 2 3 4 5 6 lhpat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑆𝐴𝑃𝑆 ) ) → 𝐶𝐴 )