Metamath Proof Explorer

Theorem lplnnle2at

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

Ref Expression
Hypotheses lplnnle2at.l 
|- .<_ = ( le ` K )
lplnnle2at.j 
|- .\/ = ( join ` K )
lplnnle2at.a 
|- A = ( Atoms ` K )
lplnnle2at.p 
|- P = ( LPlanes ` K )
Assertion lplnnle2at 
|- ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) ) -> -. X .<_ ( Q .\/ R ) )

Proof

Step Hyp Ref Expression
1 lplnnle2at.l 
 |-  .<_ = ( le ` K )
2 lplnnle2at.j 
 |-  .\/ = ( join ` K )
3 lplnnle2at.a 
 |-  A = ( Atoms ` K )
4 lplnnle2at.p 
 |-  P = ( LPlanes ` K )
5 simpr1 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) ) -> X e. P )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 eqid 
 |-  (
8 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
9 6 7 8 4 islpln 
 |-  ( K e. HL -> ( X e. P <-> ( X e. ( Base ` K ) /\ E. y e. ( LLines ` K ) y (
10 9 adantr 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) ) -> ( X e. P <-> ( X e. ( Base ` K ) /\ E. y e. ( LLines ` K ) y (
11 5 10 mpbid 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) ) -> ( X e. ( Base ` K ) /\ E. y e. ( LLines ` K ) y (
12 11 simprd 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) ) -> E. y e. ( LLines ` K ) y (
13 oveq1 
 |-  ( Q = R -> ( Q .\/ R ) = ( R .\/ R ) )
14 13 breq2d 
 |-  ( Q = R -> ( X .<_ ( Q .\/ R ) <-> X .<_ ( R .\/ R ) ) )
15 14 notbid 
 |-  ( Q = R -> ( -. X .<_ ( Q .\/ R ) <-> -. X .<_ ( R .\/ R ) ) )
16 simpl1 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  K e. HL )
17 simpl3l 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  y e. ( LLines ` K ) )
18 simpl22 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  Q e. A )
19 simpl23 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  R e. A )
20 simpr 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  Q =/= R )
21 2 3 8 llni2 
 |-  ( ( ( K e. HL /\ Q e. A /\ R e. A ) /\ Q =/= R ) -> ( Q .\/ R ) e. ( LLines ` K ) )
22 16 18 19 20 21 syl31anc 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( Q .\/ R ) e. ( LLines ` K ) )
23 eqid 
 |-  ( lt ` K ) = ( lt ` K )
24 23 8 llnnlt 
 |-  ( ( K e. HL /\ y e. ( LLines ` K ) /\ ( Q .\/ R ) e. ( LLines ` K ) ) -> -. y ( lt ` K ) ( Q .\/ R ) )
25 16 17 22 24 syl3anc 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  -. y ( lt ` K ) ( Q .\/ R ) )
26 6 8 llnbase 
 |-  ( y e. ( LLines ` K ) -> y e. ( Base ` K ) )
27 17 26 syl 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  y e. ( Base ` K ) )
28 simpl21 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  X e. P )
29 6 4 lplnbase 
 |-  ( X e. P -> X e. ( Base ` K ) )
30 28 29 syl 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  X e. ( Base ` K ) )
31 simpl3r 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  y (
32 6 23 7 cvrlt 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ X e. ( Base ` K ) ) /\ y (  y ( lt ` K ) X )
33 16 27 30 31 32 syl31anc 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  y ( lt ` K ) X )
34 hlpos 
 |-  ( K e. HL -> K e. Poset )
35 16 34 syl 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  K e. Poset )
36 6 2 3 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
37 16 18 19 36 syl3anc 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( Q .\/ R ) e. ( Base ` K ) )
38 6 1 23 pltletr 
 |-  ( ( K e. Poset /\ ( y e. ( Base ` K ) /\ X e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) ) -> ( ( y ( lt ` K ) X /\ X .<_ ( Q .\/ R ) ) -> y ( lt ` K ) ( Q .\/ R ) ) )
39 35 27 30 37 38 syl13anc 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( ( y ( lt ` K ) X /\ X .<_ ( Q .\/ R ) ) -> y ( lt ` K ) ( Q .\/ R ) ) )
40 33 39 mpand 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( X .<_ ( Q .\/ R ) -> y ( lt ` K ) ( Q .\/ R ) ) )
41 25 40 mtod 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  -. X .<_ ( Q .\/ R ) )
42 simp1 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  K e. HL )
43 simp3l 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  y e. ( LLines ` K ) )
44 simp23 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  R e. A )
45 1 3 8 llnnleat 
 |-  ( ( K e. HL /\ y e. ( LLines ` K ) /\ R e. A ) -> -. y .<_ R )
46 42 43 44 45 syl3anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  -. y .<_ R )
47 43 26 syl 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  y e. ( Base ` K ) )
48 simp21 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  X e. P )
49 48 29 syl 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  X e. ( Base ` K ) )
50 simp3r 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  y (
51 42 47 49 50 32 syl31anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  y ( lt ` K ) X )
52 34 3ad2ant1 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  K e. Poset )
53 6 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
54 44 53 syl 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  R e. ( Base ` K ) )
55 6 1 23 pltletr 
 |-  ( ( K e. Poset /\ ( y e. ( Base ` K ) /\ X e. ( Base ` K ) /\ R e. ( Base ` K ) ) ) -> ( ( y ( lt ` K ) X /\ X .<_ R ) -> y ( lt ` K ) R ) )
56 52 47 49 54 55 syl13anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( ( y ( lt ` K ) X /\ X .<_ R ) -> y ( lt ` K ) R ) )
57 51 56 mpand 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( X .<_ R -> y ( lt ` K ) R ) )
58 1 23 pltle 
 |-  ( ( K e. HL /\ y e. ( LLines ` K ) /\ R e. A ) -> ( y ( lt ` K ) R -> y .<_ R ) )
59 42 43 44 58 syl3anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( y ( lt ` K ) R -> y .<_ R ) )
60 57 59 syld 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( X .<_ R -> y .<_ R ) )
61 46 60 mtod 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  -. X .<_ R )
62 2 3 hlatjidm 
 |-  ( ( K e. HL /\ R e. A ) -> ( R .\/ R ) = R )
63 42 44 62 syl2anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( R .\/ R ) = R )
64 63 breq2d 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  ( X .<_ ( R .\/ R ) <-> X .<_ R ) )
65 61 64 mtbird 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  -. X .<_ ( R .\/ R ) )
66 15 41 65 pm2.61ne 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) /\ ( y e. ( LLines ` K ) /\ y (  -. X .<_ ( Q .\/ R ) )
67 66 3exp 
 |-  ( K e. HL -> ( ( X e. P /\ Q e. A /\ R e. A ) -> ( ( y e. ( LLines ` K ) /\ y (  -. X .<_ ( Q .\/ R ) ) ) )
68 67 exp4a 
 |-  ( K e. HL -> ( ( X e. P /\ Q e. A /\ R e. A ) -> ( y e. ( LLines ` K ) -> ( y (  -. X .<_ ( Q .\/ R ) ) ) ) )
69 68 imp 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) ) -> ( y e. ( LLines ` K ) -> ( y (  -. X .<_ ( Q .\/ R ) ) ) )
70 69 rexlimdv 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) ) -> ( E. y e. ( LLines ` K ) y (  -. X .<_ ( Q .\/ R ) ) )
71 12 70 mpd 
 |-  ( ( K e. HL /\ ( X e. P /\ Q e. A /\ R e. A ) ) -> -. X .<_ ( Q .\/ R ) )