Metamath Proof Explorer


Theorem lplnnelln

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

Ref Expression
Hypotheses lplnnelln.n N = LLines K
lplnnelln.p P = LPlanes K
Assertion lplnnelln K HL X P ¬ X N

Proof

Step Hyp Ref Expression
1 lplnnelln.n N = LLines K
2 lplnnelln.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 lplnnlelln K HL X P X N ¬ X K X
10 9 3expia K HL X P X N ¬ X K X
11 8 10 mt2d K HL X P ¬ X N