Metamath Proof Explorer

Theorem lhp0lt

Description: A co-atom is greater than zero. TODO: is this needed? (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses lhp0lt.s ⊢ < = ( lt ‘ 𝐾 )
lhp0lt.z ⊢ 0 = ( 0. ‘ 𝐾 )
lhp0lt.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhp0lt ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 < 𝑊 )

Proof

Step Hyp Ref Expression
1 lhp0lt.s ⊢ < = ( lt ‘ 𝐾 )
2 lhp0lt.z ⊢ 0 = ( 0. ‘ 𝐾 )
3 lhp0lt.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
5 1 4 3 lhpexlt ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 < 𝑊 )
6 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 𝐾 ∈ HL )
7 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 2 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
10 6 7 9 3syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 0 ∈ ( Base ‘ 𝐾 ) )
11 8 4 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
12 11 3ad2ant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
13 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
14 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
15 2 14 4 atcvr0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 0 ( ⋖ ‘ 𝐾 ) 𝑝 )
16 6 13 15 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 0 ( ⋖ ‘ 𝐾 ) 𝑝 )
17 8 1 14 cvrlt ⊢ ( ( ( 𝐾 ∈ HL ∧ 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) ∧ 0 ( ⋖ ‘ 𝐾 ) 𝑝 ) → 0 < 𝑝 )
18 6 10 12 16 17 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 0 < 𝑝 )
19 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 𝑝 < 𝑊 )
20 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
21 6 20 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 𝐾 ∈ Poset )
22 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 𝑊 ∈ 𝐻 )
23 8 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
24 22 23 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
25 8 1 plttr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 0 < 𝑝 ∧ 𝑝 < 𝑊 ) → 0 < 𝑊 ) )
26 21 10 12 24 25 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → ( ( 0 < 𝑝 ∧ 𝑝 < 𝑊 ) → 0 < 𝑊 ) )
27 18 19 26 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 < 𝑊 ) → 0 < 𝑊 )
28 27 rexlimdv3a ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 < 𝑊 → 0 < 𝑊 ) )
29 5 28 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 < 𝑊 )