Theorem lplnnlt

Description: Two lattice planes cannot satisfy the less than relation. (Contributed by NM, 7-Jul-2012)

	Ref	Expression
Hypotheses	lplnnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	lplnnlt.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	lplnnlt	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in P\right)\to \neg X\underset{\dot{}}{<}Y$$

Proof

Step	Hyp	Ref	Expression
1		lplnnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
2		lplnnlt.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
3	1	pltirr	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\right)\to \neg X\underset{\dot{}}{<}X$$
4	3	3adant3	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in P\right)\to \neg X\underset{\dot{}}{<}X$$
5		breq2	$$⊢X=Y\to \left(X\underset{\dot{}}{<}X\leftrightarrow X\underset{\dot{}}{<}Y\right)$$
6	5	notbid	$$⊢X=Y\to \left(\neg X\underset{\dot{}}{<}X\leftrightarrow \neg X\underset{\dot{}}{<}Y\right)$$
7	4 6	syl5ibcom	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in P\right)\to \left(X=Y\to \neg X\underset{\dot{}}{<}Y\right)$$
8		eqid	$$⊢{\le }_K={\le }_K$$
9	8 1	pltle	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in P\right)\to \left(X\underset{\dot{}}{<}Y\to X{\le }_{K}Y\right)$$
10	8 2	lplncmp	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in P\right)\to \left(X{\le }_{K}Y\leftrightarrow X=Y\right)$$
11	9 10	sylibd	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in P\right)\to \left(X\underset{\dot{}}{<}Y\to X=Y\right)$$
12	11	necon3ad	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in P\right)\to \left(X\ne Y\to \neg X\underset{\dot{}}{<}Y\right)$$
13	7 12	pm2.61dne	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in P\right)\to \neg X\underset{\dot{}}{<}Y$$