Metamath Proof Explorer


Theorem llnle

Description: Any element greater than 0 and not an atom majorizes a lattice line. (Contributed by NM, 28-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 llnle.b
 |-  B = ( Base ` K )
2 llnle.l
 |-  .<_ = ( le ` K )
3 llnle.z
 |-  .0. = ( 0. ` K )
4 llnle.a
 |-  A = ( Atoms ` K )
5 llnle.n
 |-  N = ( LLines ` K )
6 simpll
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> K e. HL )
7 simplr
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> X e. B )
8 simprl
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> X =/= .0. )
9 1 2 3 4 atle
 |-  ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> E. p e. A p .<_ X )
10 6 7 8 9 syl3anc
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> E. p e. A p .<_ X )
11 simp1ll
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> K e. HL )
12 1 4 atbase
 |-  ( p e. A -> p e. B )
13 12 3ad2ant2
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p e. B )
14 simp1lr
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> X e. B )
15 simp3
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p .<_ X )
16 simp2
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p e. A )
17 simp1rr
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> -. X e. A )
18 nelne2
 |-  ( ( p e. A /\ -. X e. A ) -> p =/= X )
19 16 17 18 syl2anc
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p =/= X )
20 eqid
 |-  ( lt ` K ) = ( lt ` K )
21 2 20 pltval
 |-  ( ( K e. HL /\ p e. A /\ X e. B ) -> ( p ( lt ` K ) X <-> ( p .<_ X /\ p =/= X ) ) )
22 11 16 14 21 syl3anc
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> ( p ( lt ` K ) X <-> ( p .<_ X /\ p =/= X ) ) )
23 15 19 22 mpbir2and
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p ( lt ` K ) X )
24 eqid
 |-  ( join ` K ) = ( join ` K )
25 eqid
 |-  ( 
26 1 2 20 24 25 4 hlrelat3
 |-  ( ( ( K e. HL /\ p e. B /\ X e. B ) /\ p ( lt ` K ) X ) -> E. q e. A ( p ( 
27 11 13 14 23 26 syl31anc
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> E. q e. A ( p ( 
28 simp1ll
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p (  K e. HL )
29 simp21
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p (  p e. A )
30 simp23
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p (  q e. A )
31 1 24 4 hlatjcl
 |-  ( ( K e. HL /\ p e. A /\ q e. A ) -> ( p ( join ` K ) q ) e. B )
32 28 29 30 31 syl3anc
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p (  ( p ( join ` K ) q ) e. B )
33 simp3l
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p (  p ( 
34 1 25 4 5 llni
 |-  ( ( ( K e. HL /\ ( p ( join ` K ) q ) e. B /\ p e. A ) /\ p (  ( p ( join ` K ) q ) e. N )
35 28 32 29 33 34 syl31anc
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p (  ( p ( join ` K ) q ) e. N )
36 simp3r
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p (  ( p ( join ` K ) q ) .<_ X )
37 breq1
 |-  ( y = ( p ( join ` K ) q ) -> ( y .<_ X <-> ( p ( join ` K ) q ) .<_ X ) )
38 37 rspcev
 |-  ( ( ( p ( join ` K ) q ) e. N /\ ( p ( join ` K ) q ) .<_ X ) -> E. y e. N y .<_ X )
39 35 36 38 syl2anc
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p (  E. y e. N y .<_ X )
40 39 3exp
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> ( ( p e. A /\ p .<_ X /\ q e. A ) -> ( ( p (  E. y e. N y .<_ X ) ) )
41 40 3expd
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> ( p e. A -> ( p .<_ X -> ( q e. A -> ( ( p (  E. y e. N y .<_ X ) ) ) ) )
42 41 3imp
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> ( q e. A -> ( ( p (  E. y e. N y .<_ X ) ) )
43 42 rexlimdv
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> ( E. q e. A ( p (  E. y e. N y .<_ X ) )
44 27 43 mpd
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> E. y e. N y .<_ X )
45 44 3exp
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> ( p e. A -> ( p .<_ X -> E. y e. N y .<_ X ) ) )
46 45 rexlimdv
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> ( E. p e. A p .<_ X -> E. y e. N y .<_ X ) )
47 10 46 mpd
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> E. y e. N y .<_ X )