Theorem lvolnltN

Description: Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lvolnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	lvolnlt.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	lvolnltN	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\wedge Y\in V\right)\to \neg X\underset{\dot{}}{<}Y$$

Proof

Step	Hyp	Ref	Expression
1		lvolnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
2		lvolnlt.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
3	1	pltirr	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\right)\to \neg X\underset{\dot{}}{<}X$$
4	3	3adant3	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\wedge Y\in V\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 V\wedge Y\in V\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 V\wedge Y\in V\right)\to \left(X\underset{\dot{}}{<}Y\to X{\le }_{K}Y\right)$$
10	8 2	lvolcmp	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\wedge Y\in V\right)\to \left(X{\le }_{K}Y\leftrightarrow X=Y\right)$$
11	9 10	sylibd	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\wedge Y\in V\right)\to \left(X\underset{\dot{}}{<}Y\to X=Y\right)$$
12	11	necon3ad	$$⊢\left(K\in \mathrm{HL}\wedge X\in V\wedge Y\in V\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 V\wedge Y\in V\right)\to \neg X\underset{\dot{}}{<}Y$$