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 )