Metamath Proof Explorer

Theorem llnnleat

Description: An atom cannot majorize a lattice line. (Contributed by NM, 8-Jul-2012)

Ref Expression
Hypotheses llnnleat.l 
|- .<_ = ( le ` K )
llnnleat.a 
|- A = ( Atoms ` K )
llnnleat.n 
|- N = ( LLines ` K )
Assertion llnnleat 
|- ( ( K e. HL /\ X e. N /\ P e. A ) -> -. X .<_ P )

Proof

Step Hyp Ref Expression
1 llnnleat.l 
 |-  .<_ = ( le ` K )
2 llnnleat.a 
 |-  A = ( Atoms ` K )
3 llnnleat.n 
 |-  N = ( LLines ` K )
4 simp2 
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> X e. N )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  (
7 5 6 2 3 islln 
 |-  ( K e. HL -> ( X e. N <-> ( X e. ( Base ` K ) /\ E. q e. A q (
8 7 3ad2ant1 
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> ( X e. N <-> ( X e. ( Base ` K ) /\ E. q e. A q (
9 4 8 mpbid 
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> ( X e. ( Base ` K ) /\ E. q e. A q (
10 9 simprd 
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> E. q e. A q (
11 simp11 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  K e. HL )
12 hlatl 
 |-  ( K e. HL -> K e. AtLat )
13 11 12 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  K e. AtLat )
14 simp2 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  q e. A )
15 simp13 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  P e. A )
16 eqid 
 |-  ( lt ` K ) = ( lt ` K )
17 16 2 atnlt 
 |-  ( ( K e. AtLat /\ q e. A /\ P e. A ) -> -. q ( lt ` K ) P )
18 13 14 15 17 syl3anc 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  -. q ( lt ` K ) P )
19 5 2 atbase 
 |-  ( q e. A -> q e. ( Base ` K ) )
20 19 3ad2ant2 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  q e. ( Base ` K ) )
21 simp12 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  X e. N )
22 5 3 llnbase 
 |-  ( X e. N -> X e. ( Base ` K ) )
23 21 22 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  X e. ( Base ` K ) )
24 simp3 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  q (
25 5 16 6 cvrlt 
 |-  ( ( ( K e. HL /\ q e. ( Base ` K ) /\ X e. ( Base ` K ) ) /\ q (  q ( lt ` K ) X )
26 11 20 23 24 25 syl31anc 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  q ( lt ` K ) X )
27 hlpos 
 |-  ( K e. HL -> K e. Poset )
28 11 27 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  K e. Poset )
29 5 2 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
30 15 29 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  P e. ( Base ` K ) )
31 5 1 16 pltletr 
 |-  ( ( K e. Poset /\ ( q e. ( Base ` K ) /\ X e. ( Base ` K ) /\ P e. ( Base ` K ) ) ) -> ( ( q ( lt ` K ) X /\ X .<_ P ) -> q ( lt ` K ) P ) )
32 28 20 23 30 31 syl13anc 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  ( ( q ( lt ` K ) X /\ X .<_ P ) -> q ( lt ` K ) P ) )
33 26 32 mpand 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  ( X .<_ P -> q ( lt ` K ) P ) )
34 18 33 mtod 
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ q e. A /\ q (  -. X .<_ P )
35 34 rexlimdv3a 
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> ( E. q e. A q (  -. X .<_ P ) )
36 10 35 mpd 
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> -. X .<_ P )