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 ˙=K
lvolnle3at.j ˙=joinK
lvolnle3at.a A=AtomsK
lvolnle3at.v V=LVolsK
Assertion lvolnle3at KHLXVPAQARA¬X˙P˙Q˙R

Proof

Step Hyp Ref Expression
1 lvolnle3at.l ˙=K
2 lvolnle3at.j ˙=joinK
3 lvolnle3at.a A=AtomsK
4 lvolnle3at.v V=LVolsK
5 simplr KHLXVPAQARAXV
6 eqid BaseK=BaseK
7 eqid K=K
8 eqid LPlanesK=LPlanesK
9 6 7 8 4 islvol KHLXVXBaseKyLPlanesKyKX
10 9 ad2antrr KHLXVPAQARAXVXBaseKyLPlanesKyKX
11 5 10 mpbid KHLXVPAQARAXBaseKyLPlanesKyKX
12 11 simprd KHLXVPAQARAyLPlanesKyKX
13 oveq1 P=QP˙Q=Q˙Q
14 13 oveq1d P=QP˙Q˙R=Q˙Q˙R
15 14 breq2d P=QX˙P˙Q˙RX˙Q˙Q˙R
16 15 notbid P=Q¬X˙P˙Q˙R¬X˙Q˙Q˙R
17 simp1l KHLXVPAQARAyLPlanesKyKXKHL
18 simp3l KHLXVPAQARAyLPlanesKyKXyLPlanesK
19 simp21 KHLXVPAQARAyLPlanesKyKXPA
20 simp22 KHLXVPAQARAyLPlanesKyKXQA
21 1 2 3 8 lplnnle2at KHLyLPlanesKPAQA¬y˙P˙Q
22 17 18 19 20 21 syl13anc KHLXVPAQARAyLPlanesKyKX¬y˙P˙Q
23 6 8 lplnbase yLPlanesKyBaseK
24 18 23 syl KHLXVPAQARAyLPlanesKyKXyBaseK
25 simp1r KHLXVPAQARAyLPlanesKyKXXV
26 6 4 lvolbase XVXBaseK
27 25 26 syl KHLXVPAQARAyLPlanesKyKXXBaseK
28 simp3r KHLXVPAQARAyLPlanesKyKXyKX
29 eqid <K=<K
30 6 29 7 cvrlt KHLyBaseKXBaseKyKXy<KX
31 17 24 27 28 30 syl31anc KHLXVPAQARAyLPlanesKyKXy<KX
32 hlpos KHLKPoset
33 17 32 syl KHLXVPAQARAyLPlanesKyKXKPoset
34 6 2 3 hlatjcl KHLPAQAP˙QBaseK
35 17 19 20 34 syl3anc KHLXVPAQARAyLPlanesKyKXP˙QBaseK
36 6 1 29 pltletr KPosetyBaseKXBaseKP˙QBaseKy<KXX˙P˙Qy<KP˙Q
37 33 24 27 35 36 syl13anc KHLXVPAQARAyLPlanesKyKXy<KXX˙P˙Qy<KP˙Q
38 31 37 mpand KHLXVPAQARAyLPlanesKyKXX˙P˙Qy<KP˙Q
39 1 29 pltle KHLyLPlanesKP˙QBaseKy<KP˙Qy˙P˙Q
40 17 18 35 39 syl3anc KHLXVPAQARAyLPlanesKyKXy<KP˙Qy˙P˙Q
41 38 40 syld KHLXVPAQARAyLPlanesKyKXX˙P˙Qy˙P˙Q
42 22 41 mtod KHLXVPAQARAyLPlanesKyKX¬X˙P˙Q
43 42 adantr KHLXVPAQARAyLPlanesKyKXPQR˙P˙Q¬X˙P˙Q
44 simprr KHLXVPAQARAyLPlanesKyKXPQR˙P˙QR˙P˙Q
45 17 hllatd KHLXVPAQARAyLPlanesKyKXKLat
46 simp23 KHLXVPAQARAyLPlanesKyKXRA
47 6 3 atbase RARBaseK
48 46 47 syl KHLXVPAQARAyLPlanesKyKXRBaseK
49 6 1 2 latleeqj2 KLatRBaseKP˙QBaseKR˙P˙QP˙Q˙R=P˙Q
50 45 48 35 49 syl3anc KHLXVPAQARAyLPlanesKyKXR˙P˙QP˙Q˙R=P˙Q
51 50 adantr KHLXVPAQARAyLPlanesKyKXPQR˙P˙QR˙P˙QP˙Q˙R=P˙Q
52 44 51 mpbid KHLXVPAQARAyLPlanesKyKXPQR˙P˙QP˙Q˙R=P˙Q
53 52 breq2d KHLXVPAQARAyLPlanesKyKXPQR˙P˙QX˙P˙Q˙RX˙P˙Q
54 43 53 mtbird KHLXVPAQARAyLPlanesKyKXPQR˙P˙Q¬X˙P˙Q˙R
55 54 anassrs KHLXVPAQARAyLPlanesKyKXPQR˙P˙Q¬X˙P˙Q˙R
56 simpl1l KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙QKHL
57 simpl3l KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙QyLPlanesK
58 simpl2 KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙QPAQARA
59 simpr KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙QPQ¬R˙P˙Q
60 1 2 3 8 lplni2 KHLPAQARAPQ¬R˙P˙QP˙Q˙RLPlanesK
61 56 58 59 60 syl3anc KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙QP˙Q˙RLPlanesK
62 29 8 lplnnlt KHLyLPlanesKP˙Q˙RLPlanesK¬y<KP˙Q˙R
63 56 57 61 62 syl3anc KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙Q¬y<KP˙Q˙R
64 6 2 latjcl KLatP˙QBaseKRBaseKP˙Q˙RBaseK
65 45 35 48 64 syl3anc KHLXVPAQARAyLPlanesKyKXP˙Q˙RBaseK
66 6 1 29 pltletr KPosetyBaseKXBaseKP˙Q˙RBaseKy<KXX˙P˙Q˙Ry<KP˙Q˙R
67 33 24 27 65 66 syl13anc KHLXVPAQARAyLPlanesKyKXy<KXX˙P˙Q˙Ry<KP˙Q˙R
68 31 67 mpand KHLXVPAQARAyLPlanesKyKXX˙P˙Q˙Ry<KP˙Q˙R
69 68 adantr KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙QX˙P˙Q˙Ry<KP˙Q˙R
70 63 69 mtod KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙Q¬X˙P˙Q˙R
71 70 anassrs KHLXVPAQARAyLPlanesKyKXPQ¬R˙P˙Q¬X˙P˙Q˙R
72 55 71 pm2.61dan KHLXVPAQARAyLPlanesKyKXPQ¬X˙P˙Q˙R
73 eqid K=K
74 73 2 3 8 lplnnle2at KHLyLPlanesKQARA¬yKQ˙R
75 17 18 20 46 74 syl13anc KHLXVPAQARAyLPlanesKyKX¬yKQ˙R
76 6 2 3 hlatjcl KHLQARAQ˙RBaseK
77 17 20 46 76 syl3anc KHLXVPAQARAyLPlanesKyKXQ˙RBaseK
78 6 1 29 pltletr KPosetyBaseKXBaseKQ˙RBaseKy<KXX˙Q˙Ry<KQ˙R
79 33 24 27 77 78 syl13anc KHLXVPAQARAyLPlanesKyKXy<KXX˙Q˙Ry<KQ˙R
80 31 79 mpand KHLXVPAQARAyLPlanesKyKXX˙Q˙Ry<KQ˙R
81 73 29 pltle KHLyLPlanesKQ˙RBaseKy<KQ˙RyKQ˙R
82 17 18 77 81 syl3anc KHLXVPAQARAyLPlanesKyKXy<KQ˙RyKQ˙R
83 80 82 syld KHLXVPAQARAyLPlanesKyKXX˙Q˙RyKQ˙R
84 75 83 mtod KHLXVPAQARAyLPlanesKyKX¬X˙Q˙R
85 2 3 hlatjidm KHLQAQ˙Q=Q
86 17 20 85 syl2anc KHLXVPAQARAyLPlanesKyKXQ˙Q=Q
87 86 oveq1d KHLXVPAQARAyLPlanesKyKXQ˙Q˙R=Q˙R
88 87 breq2d KHLXVPAQARAyLPlanesKyKXX˙Q˙Q˙RX˙Q˙R
89 84 88 mtbird KHLXVPAQARAyLPlanesKyKX¬X˙Q˙Q˙R
90 16 72 89 pm2.61ne KHLXVPAQARAyLPlanesKyKX¬X˙P˙Q˙R
91 90 3expia KHLXVPAQARAyLPlanesKyKX¬X˙P˙Q˙R
92 91 expd KHLXVPAQARAyLPlanesKyKX¬X˙P˙Q˙R
93 92 rexlimdv KHLXVPAQARAyLPlanesKyKX¬X˙P˙Q˙R
94 12 93 mpd KHLXVPAQARA¬X˙P˙Q˙R