Metamath Proof Explorer


Theorem lplnneat

Description: No lattice plane is an atom. (Contributed by NM, 15-Jul-2012)

Ref Expression
Hypotheses lplnneat.a A = Atoms K
lplnneat.p P = LPlanes K
Assertion lplnneat K HL X P ¬ X A

Proof

Step Hyp Ref Expression
1 lplnneat.a A = Atoms K
2 lplnneat.p P = LPlanes K
3 hllat K HL K Lat
4 eqid Base K = Base K
5 4 2 lplnbase X P 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 P X K X
9 6 1 2 lplnnleat K HL X P X A ¬ X K X
10 9 3expia K HL X P X A ¬ X K X
11 8 10 mt2d K HL X P ¬ X A