Metamath Proof Explorer

Theorem lplnle

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

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

Proof

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