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

Metamath Proof Explorer

Theorem lhplt

Description: An atom under a co-atom is strictly less than it. TODO: is this needed? (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses lhplt.l ⊢ ≤ ˙ = ≤ K
lhplt.s ⊢ < ˙ = < K
lhplt.a ⊢ A = Atoms ⁡ K
lhplt.h ⊢ H = LHyp ⁡ K
Assertion lhplt ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ P ≤ ˙ W → P < ˙ W

Proof

Step Hyp Ref Expression
1 lhplt.l ⊢ ≤ ˙ = ≤ K
2 lhplt.s ⊢ < ˙ = < K
3 lhplt.a ⊢ A = Atoms ⁡ K
4 lhplt.h ⊢ H = LHyp ⁡ K
5 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ P ≤ ˙ W → K ∈ HL
6 simprl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ P ≤ ˙ W → P ∈ A
7 eqid ⊢ Base K = Base K
8 7 4 lhpbase ⊢ W ∈ H → W ∈ Base K
9 8 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ P ≤ ˙ W → W ∈ Base K
10 eqid ⊢ 1. ⁡ K = 1. ⁡ K
11 eqid ⊢ ⋖ K = ⋖ K
12 10 11 4 lhp1cvr ⊢ K ∈ HL ∧ W ∈ H → W ⋖ K 1. ⁡ K
13 12 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ P ≤ ˙ W → W ⋖ K 1. ⁡ K
14 simprr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ P ≤ ˙ W → P ≤ ˙ W
15 7 1 2 10 11 3 1cvratlt ⊢ K ∈ HL ∧ P ∈ A ∧ W ∈ Base K ∧ W ⋖ K 1. ⁡ K ∧ P ≤ ˙ W → P < ˙ W
16 5 6 9 13 14 15 syl32anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ P ≤ ˙ W → P < ˙ W