This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 𝑝 < 𝑊 )