Metamath Proof Explorer

Theorem atle

Description: Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012)

Ref Expression
Hypotheses atle.b 
|- B = ( Base ` K )
atle.l 
|- .<_ = ( le ` K )
atle.z 
|- .0. = ( 0. ` K )
atle.a 
|- A = ( Atoms ` K )
Assertion atle 
|- ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> E. p e. A p .<_ X )

Proof

Step Hyp Ref Expression
1 atle.b 
 |-  B = ( Base ` K )
2 atle.l 
 |-  .<_ = ( le ` K )
3 atle.z 
 |-  .0. = ( 0. ` K )
4 atle.a 
 |-  A = ( Atoms ` K )
5 simp1 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> K e. HL )
6 hlop 
 |-  ( K e. HL -> K e. OP )
7 6 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> K e. OP )
8 1 3 op0cl 
 |-  ( K e. OP -> .0. e. B )
9 7 8 syl 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> .0. e. B )
10 simp2 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> X e. B )
11 simp3 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> X =/= .0. )
12 eqid 
 |-  ( lt ` K ) = ( lt ` K )
13 1 12 3 opltn0 
 |-  ( ( K e. OP /\ X e. B ) -> ( .0. ( lt ` K ) X <-> X =/= .0. ) )
14 7 10 13 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> ( .0. ( lt ` K ) X <-> X =/= .0. ) )
15 11 14 mpbird 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> .0. ( lt ` K ) X )
16 eqid 
 |-  ( join ` K ) = ( join ` K )
17 1 2 12 16 4 hlrelat 
 |-  ( ( ( K e. HL /\ .0. e. B /\ X e. B ) /\ .0. ( lt ` K ) X ) -> E. p e. A ( .0. ( lt ` K ) ( .0. ( join ` K ) p ) /\ ( .0. ( join ` K ) p ) .<_ X ) )
18 5 9 10 15 17 syl31anc 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> E. p e. A ( .0. ( lt ` K ) ( .0. ( join ` K ) p ) /\ ( .0. ( join ` K ) p ) .<_ X ) )
19 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ X =/= .0. ) /\ p e. A ) -> K e. HL )
20 hlol 
 |-  ( K e. HL -> K e. OL )
21 19 20 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ X =/= .0. ) /\ p e. A ) -> K e. OL )
22 1 4 atbase 
 |-  ( p e. A -> p e. B )
23 22 adantl 
 |-  ( ( ( K e. HL /\ X e. B /\ X =/= .0. ) /\ p e. A ) -> p e. B )
24 1 16 3 olj02 
 |-  ( ( K e. OL /\ p e. B ) -> ( .0. ( join ` K ) p ) = p )
25 21 23 24 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X =/= .0. ) /\ p e. A ) -> ( .0. ( join ` K ) p ) = p )
26 25 breq1d 
 |-  ( ( ( K e. HL /\ X e. B /\ X =/= .0. ) /\ p e. A ) -> ( ( .0. ( join ` K ) p ) .<_ X <-> p .<_ X ) )
27 26 biimpd 
 |-  ( ( ( K e. HL /\ X e. B /\ X =/= .0. ) /\ p e. A ) -> ( ( .0. ( join ` K ) p ) .<_ X -> p .<_ X ) )
28 27 adantld 
 |-  ( ( ( K e. HL /\ X e. B /\ X =/= .0. ) /\ p e. A ) -> ( ( .0. ( lt ` K ) ( .0. ( join ` K ) p ) /\ ( .0. ( join ` K ) p ) .<_ X ) -> p .<_ X ) )
29 28 reximdva 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> ( E. p e. A ( .0. ( lt ` K ) ( .0. ( join ` K ) p ) /\ ( .0. ( join ` K ) p ) .<_ X ) -> E. p e. A p .<_ X ) )
30 18 29 mpd 
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> E. p e. A p .<_ X )