Theorem lvolnelpln

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

	Ref	Expression
Hypotheses	lvolnelpln.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
	lvolnelpln.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	lvolnelpln	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\right)\to \neg X\in P$$

Proof

Step	Hyp	Ref	Expression
1		lvolnelpln.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
2		lvolnelpln.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
3		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	4 2	lvolbase	$$⊢X\in V\to X\in {\mathrm{Base}}_K$$
6		eqid	$$⊢{\le }_K={\le }_K$$
7	4 6	latref	$$⊢\left(K\in \mathrm{Lat}\wedge X\in {\mathrm{Base}}_K\right)\to X{\le }_{K}X$$
8	3 5 7	syl2an	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\right)\to X{\le }_{K}X$$
9	6 1 2	lvolnlelpln	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\wedge X\in P\right)\to \neg X{\le }_{K}X$$
10	9	3expia	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\right)\to \left(X\in P\to \neg X{\le }_{K}X\right)$$
11	8 10	mt2d	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\right)\to \neg X\in P$$