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=AtomsK
lhplt.h H=LHypK
Assertion lhplt KHLWHPAP˙WP<˙W

Proof

Step Hyp Ref Expression
1 lhplt.l ˙=K
2 lhplt.s <˙=<K
3 lhplt.a A=AtomsK
4 lhplt.h H=LHypK
5 simpll KHLWHPAP˙WKHL
6 simprl KHLWHPAP˙WPA
7 eqid BaseK=BaseK
8 7 4 lhpbase WHWBaseK
9 8 ad2antlr KHLWHPAP˙WWBaseK
10 eqid 1.K=1.K
11 eqid K=K
12 10 11 4 lhp1cvr KHLWHWK1.K
13 12 adantr KHLWHPAP˙WWK1.K
14 simprr KHLWHPAP˙WP˙W
15 7 1 2 10 11 3 1cvratlt KHLPAWBaseKWK1.KP˙WP<˙W
16 5 6 9 13 14 15 syl32anc KHLWHPAP˙WP<˙W