Metamath Proof Explorer


Theorem lvolnelpln

Description: No lattice volume is a lattice plane. (Contributed by NM, 19-Jun-2012)

Ref Expression
Hypotheses lvolnelpln.p P = LPlanes K
lvolnelpln.v V = LVols K
Assertion lvolnelpln K HL X V ¬ X P

Proof

Step Hyp Ref Expression
1 lvolnelpln.p P = LPlanes K
2 lvolnelpln.v V = LVols K
3 hllat K HL K Lat
4 eqid Base K = Base K
5 4 2 lvolbase X V X Base K
6 eqid K = K
7 4 6 latref K Lat X Base K X K X
8 3 5 7 syl2an K HL X V X K X
9 6 1 2 lvolnlelpln K HL X V X P ¬ X K X
10 9 3expia K HL X V X P ¬ X K X
11 8 10 mt2d K HL X V ¬ X P