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 ` K )
lhp0lt.z 
|- .0. = ( 0. ` K )
lhp0lt.h 
|- H = ( LHyp ` K )
Assertion lhp0lt 
|- ( ( K e. HL /\ W e. H ) -> .0. .< W )

Proof

Step Hyp Ref Expression
1 lhp0lt.s 
 |-  .< = ( lt ` K )
2 lhp0lt.z 
 |-  .0. = ( 0. ` K )
3 lhp0lt.h 
 |-  H = ( LHyp ` K )
4 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
5 1 4 3 lhpexlt 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. ( Atoms ` K ) p .< W )
6 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> K e. HL )
7 hlop 
 |-  ( K e. HL -> K e. OP )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 8 2 op0cl 
 |-  ( K e. OP -> .0. e. ( Base ` K ) )
10 6 7 9 3syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> .0. e. ( Base ` K ) )
11 8 4 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. ( Base ` K ) )
12 11 3ad2ant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> p e. ( Base ` K ) )
13 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> p e. ( Atoms ` K ) )
14 eqid 
 |-  (
15 2 14 4 atcvr0 
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) ) -> .0. (
16 6 13 15 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> .0. (
17 8 1 14 cvrlt 
 |-  ( ( ( K e. HL /\ .0. e. ( Base ` K ) /\ p e. ( Base ` K ) ) /\ .0. (  .0. .< p )
18 6 10 12 16 17 syl31anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> .0. .< p )
19 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> p .< W )
20 hlpos 
 |-  ( K e. HL -> K e. Poset )
21 6 20 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> K e. Poset )
22 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> W e. H )
23 8 3 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
24 22 23 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> W e. ( Base ` K ) )
25 8 1 plttr 
 |-  ( ( K e. Poset /\ ( .0. e. ( Base ` K ) /\ p e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( .0. .< p /\ p .< W ) -> .0. .< W ) )
26 21 10 12 24 25 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> ( ( .0. .< p /\ p .< W ) -> .0. .< W ) )
27 18 19 26 mp2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ( Atoms ` K ) /\ p .< W ) -> .0. .< W )
28 27 rexlimdv3a 
 |-  ( ( K e. HL /\ W e. H ) -> ( E. p e. ( Atoms ` K ) p .< W -> .0. .< W ) )
29 5 28 mpd 
 |-  ( ( K e. HL /\ W e. H ) -> .0. .< W )