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 ` K )
	lhplt.s	|- .< = ( lt ` K )
	lhplt.a	|- A = ( Atoms ` K )
	lhplt.h	|- H = ( LHyp ` K )
Assertion	lhplt	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) ) -> P .< W )

Proof

Step	Hyp	Ref	Expression
1		lhplt.l	|- .<_ = ( le ` K )
2		lhplt.s	|- .< = ( lt ` K )
3		lhplt.a	|- A = ( Atoms ` K )
4		lhplt.h	|- H = ( LHyp ` K )
5		simpll	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) ) -> K e. HL )
6		simprl	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) ) -> P e. A )
7		eqid	|- ( Base ` K ) = ( Base ` K )
8	7 4	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
9	8	ad2antlr	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) ) -> W e. ( Base ` K ) )
10		eqid	|- ( 1. ` K ) = ( 1. ` K )
11		eqid	|- (
12	10 11 4	lhp1cvr	|- ( ( K e. HL /\ W e. H ) -> W (
13	12	adantr	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) ) -> W (
14		simprr	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) ) -> P .<_ W )
15	7 1 2 10 11 3	1cvratlt	|- ( ( ( K e. HL /\ P e. A /\ W e. ( Base ` K ) ) /\ ( W ( P .< W )
16	5 6 9 13 14 15	syl32anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) ) -> P .< W )