Metamath Proof Explorer


Theorem lhpexlt

Description: There exists an atom less than a co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses lhpatltex.s < = ( lt ‘ 𝐾 )
lhpatltex.a 𝐴 = ( Atoms ‘ 𝐾 )
lhpatltex.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexlt ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 𝑝 < 𝑊 )

Proof

Step Hyp Ref Expression
1 lhpatltex.s < = ( lt ‘ 𝐾 )
2 lhpatltex.a 𝐴 = ( Atoms ‘ 𝐾 )
3 lhpatltex.h 𝐻 = ( LHyp ‘ 𝐾 )
4 simpl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐾 ∈ HL )
5 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 5 3 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
7 6 adantl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
8 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
9 eqid ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
10 8 9 3 lhp1cvr ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
11 5 1 8 9 2 1cvratex ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ∃ 𝑝𝐴 𝑝 < 𝑊 )
12 4 7 10 11 syl3anc ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 𝑝 < 𝑊 )