Metamath Proof Explorer

Theorem lvolnle3at

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

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

Proof

Step Hyp Ref Expression
1 lvolnle3at.l 
 |-  .<_ = ( le ` K )
2 lvolnle3at.j 
 |-  .\/ = ( join ` K )
3 lvolnle3at.a 
 |-  A = ( Atoms ` K )
4 lvolnle3at.v 
 |-  V = ( LVols ` K )
5 simplr 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> X e. V )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 eqid 
 |-  (
8 eqid 
 |-  ( LPlanes ` K ) = ( LPlanes ` K )
9 6 7 8 4 islvol 
 |-  ( K e. HL -> ( X e. V <-> ( X e. ( Base ` K ) /\ E. y e. ( LPlanes ` K ) y (
10 9 ad2antrr 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( X e. V <-> ( X e. ( Base ` K ) /\ E. y e. ( LPlanes ` K ) y (
11 5 10 mpbid 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( X e. ( Base ` K ) /\ E. y e. ( LPlanes ` K ) y (
12 11 simprd 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> E. y e. ( LPlanes ` K ) y (
13 oveq1 
 |-  ( P = Q -> ( P .\/ Q ) = ( Q .\/ Q ) )
14 13 oveq1d 
 |-  ( P = Q -> ( ( P .\/ Q ) .\/ R ) = ( ( Q .\/ Q ) .\/ R ) )
15 14 breq2d 
 |-  ( P = Q -> ( X .<_ ( ( P .\/ Q ) .\/ R ) <-> X .<_ ( ( Q .\/ Q ) .\/ R ) ) )
16 15 notbid 
 |-  ( P = Q -> ( -. X .<_ ( ( P .\/ Q ) .\/ R ) <-> -. X .<_ ( ( Q .\/ Q ) .\/ R ) ) )
17 simp1l 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  K e. HL )
18 simp3l 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  y e. ( LPlanes ` K ) )
19 simp21 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  P e. A )
20 simp22 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  Q e. A )
21 1 2 3 8 lplnnle2at 
 |-  ( ( K e. HL /\ ( y e. ( LPlanes ` K ) /\ P e. A /\ Q e. A ) ) -> -. y .<_ ( P .\/ Q ) )
22 17 18 19 20 21 syl13anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. y .<_ ( P .\/ Q ) )
23 6 8 lplnbase 
 |-  ( y e. ( LPlanes ` K ) -> y e. ( Base ` K ) )
24 18 23 syl 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  y e. ( Base ` K ) )
25 simp1r 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  X e. V )
26 6 4 lvolbase 
 |-  ( X e. V -> X e. ( Base ` K ) )
27 25 26 syl 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  X e. ( Base ` K ) )
28 simp3r 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  y (
29 eqid 
 |-  ( lt ` K ) = ( lt ` K )
30 6 29 7 cvrlt 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ X e. ( Base ` K ) ) /\ y (  y ( lt ` K ) X )
31 17 24 27 28 30 syl31anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  y ( lt ` K ) X )
32 hlpos 
 |-  ( K e. HL -> K e. Poset )
33 17 32 syl 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  K e. Poset )
34 6 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
35 17 19 20 34 syl3anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( P .\/ Q ) e. ( Base ` K ) )
36 6 1 29 pltletr 
 |-  ( ( K e. Poset /\ ( y e. ( Base ` K ) /\ X e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( y ( lt ` K ) X /\ X .<_ ( P .\/ Q ) ) -> y ( lt ` K ) ( P .\/ Q ) ) )
37 33 24 27 35 36 syl13anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( ( y ( lt ` K ) X /\ X .<_ ( P .\/ Q ) ) -> y ( lt ` K ) ( P .\/ Q ) ) )
38 31 37 mpand 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( X .<_ ( P .\/ Q ) -> y ( lt ` K ) ( P .\/ Q ) ) )
39 1 29 pltle 
 |-  ( ( K e. HL /\ y e. ( LPlanes ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( y ( lt ` K ) ( P .\/ Q ) -> y .<_ ( P .\/ Q ) ) )
40 17 18 35 39 syl3anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( y ( lt ` K ) ( P .\/ Q ) -> y .<_ ( P .\/ Q ) ) )
41 38 40 syld 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( X .<_ ( P .\/ Q ) -> y .<_ ( P .\/ Q ) ) )
42 22 41 mtod 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( P .\/ Q ) )
43 42 adantr 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( P .\/ Q ) )
44 simprr 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  R .<_ ( P .\/ Q ) )
45 17 hllatd 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  K e. Lat )
46 simp23 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  R e. A )
47 6 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
48 46 47 syl 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  R e. ( Base ` K ) )
49 6 1 2 latleeqj2 
 |-  ( ( K e. Lat /\ R e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( R .<_ ( P .\/ Q ) <-> ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) ) )
50 45 48 35 49 syl3anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( R .<_ ( P .\/ Q ) <-> ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) ) )
51 50 adantr 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( R .<_ ( P .\/ Q ) <-> ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) ) )
52 44 51 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) )
53 52 breq2d 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( X .<_ ( ( P .\/ Q ) .\/ R ) <-> X .<_ ( P .\/ Q ) ) )
54 43 53 mtbird 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) )
55 54 anassrs 
 |-  ( ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) )
56 simpl1l 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  K e. HL )
57 simpl3l 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  y e. ( LPlanes ` K ) )
58 simpl2 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( P e. A /\ Q e. A /\ R e. A ) )
59 simpr 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) )
60 1 2 3 8 lplni2 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( LPlanes ` K ) )
61 56 58 59 60 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( ( P .\/ Q ) .\/ R ) e. ( LPlanes ` K ) )
62 29 8 lplnnlt 
 |-  ( ( K e. HL /\ y e. ( LPlanes ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( LPlanes ` K ) ) -> -. y ( lt ` K ) ( ( P .\/ Q ) .\/ R ) )
63 56 57 61 62 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. y ( lt ` K ) ( ( P .\/ Q ) .\/ R ) )
64 6 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
65 45 35 48 64 syl3anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
66 6 1 29 pltletr 
 |-  ( ( K e. Poset /\ ( y e. ( Base ` K ) /\ X e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) ) -> ( ( y ( lt ` K ) X /\ X .<_ ( ( P .\/ Q ) .\/ R ) ) -> y ( lt ` K ) ( ( P .\/ Q ) .\/ R ) ) )
67 33 24 27 65 66 syl13anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( ( y ( lt ` K ) X /\ X .<_ ( ( P .\/ Q ) .\/ R ) ) -> y ( lt ` K ) ( ( P .\/ Q ) .\/ R ) ) )
68 31 67 mpand 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( X .<_ ( ( P .\/ Q ) .\/ R ) -> y ( lt ` K ) ( ( P .\/ Q ) .\/ R ) ) )
69 68 adantr 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( X .<_ ( ( P .\/ Q ) .\/ R ) -> y ( lt ` K ) ( ( P .\/ Q ) .\/ R ) ) )
70 63 69 mtod 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) )
71 70 anassrs 
 |-  ( ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) )
72 55 71 pm2.61dan 
 |-  ( ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) )
73 eqid 
 |-  ( le ` K ) = ( le ` K )
74 73 2 3 8 lplnnle2at 
 |-  ( ( K e. HL /\ ( y e. ( LPlanes ` K ) /\ Q e. A /\ R e. A ) ) -> -. y ( le ` K ) ( Q .\/ R ) )
75 17 18 20 46 74 syl13anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. y ( le ` K ) ( Q .\/ R ) )
76 6 2 3 hlatjcl 
 |-  ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
77 17 20 46 76 syl3anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( Q .\/ R ) e. ( Base ` K ) )
78 6 1 29 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 ) ) )
79 33 24 27 77 78 syl13anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( ( y ( lt ` K ) X /\ X .<_ ( Q .\/ R ) ) -> y ( lt ` K ) ( Q .\/ R ) ) )
80 31 79 mpand 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( X .<_ ( Q .\/ R ) -> y ( lt ` K ) ( Q .\/ R ) ) )
81 73 29 pltle 
 |-  ( ( K e. HL /\ y e. ( LPlanes ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) -> ( y ( lt ` K ) ( Q .\/ R ) -> y ( le ` K ) ( Q .\/ R ) ) )
82 17 18 77 81 syl3anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( y ( lt ` K ) ( Q .\/ R ) -> y ( le ` K ) ( Q .\/ R ) ) )
83 80 82 syld 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( X .<_ ( Q .\/ R ) -> y ( le ` K ) ( Q .\/ R ) ) )
84 75 83 mtod 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( Q .\/ R ) )
85 2 3 hlatjidm 
 |-  ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
86 17 20 85 syl2anc 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( Q .\/ Q ) = Q )
87 86 oveq1d 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( ( Q .\/ Q ) .\/ R ) = ( Q .\/ R ) )
88 87 breq2d 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  ( X .<_ ( ( Q .\/ Q ) .\/ R ) <-> X .<_ ( Q .\/ R ) ) )
89 84 88 mtbird 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( ( Q .\/ Q ) .\/ R ) )
90 16 72 89 pm2.61ne 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) )
91 90 3expia 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( y e. ( LPlanes ` K ) /\ y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) ) )
92 91 expd 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( y e. ( LPlanes ` K ) -> ( y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) ) ) )
93 92 rexlimdv 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( E. y e. ( LPlanes ` K ) y (  -. X .<_ ( ( P .\/ Q ) .\/ R ) ) )
94 12 93 mpd 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> -. X .<_ ( ( P .\/ Q ) .\/ R ) )