Metamath Proof Explorer


Theorem lvolneatN

Description: No lattice volume is an atom. (Contributed by NM, 15-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lvolneat.a A = Atoms K
lvolneat.v V = LVols K
Assertion lvolneatN K HL X V ¬ X A

Proof

Step Hyp Ref Expression
1 lvolneat.a A = Atoms K
2 lvolneat.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 lvolnleat K HL X V X A ¬ X K X
10 9 3expia K HL X V X A ¬ X K X
11 8 10 mt2d K HL X V ¬ X A