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	⊢ ≤ = ( le ‘ 𝐾 )
	lhplt.s	⊢ < = ( lt ‘ 𝐾 )
	lhplt.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lhplt.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	lhplt	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ) → 𝑃 < 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		lhplt.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lhplt.s	⊢ < = ( lt ‘ 𝐾 )
3		lhplt.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		lhplt.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
6		simprl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8	7 4	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
9	8	ad2antlr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
10		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
11		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
12	10 11 4	lhp1cvr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
13	12	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
14		simprr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ) → 𝑃 ≤ 𝑊 )
15	7 1 2 10 11 3	1cvratlt	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ∧ 𝑃 ≤ 𝑊 ) ) → 𝑃 < 𝑊 )
16	5 6 9 13 14 15	syl32anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ) → 𝑃 < 𝑊 )