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{˙}{<} = <_{K}$
	lvolnlt.v	$⊢ V = LVols (K)$
Assertion	lvolnltN	$⊢ (K \in HL \land X \in V \land Y \in V) \to \neg X \underset{˙}{<} Y$

Step	Hyp	Ref	Expression
1		lvolnlt.s	$⊢ \underset{˙}{<} = <_{K}$
2		lvolnlt.v	$⊢ V = LVols (K)$
3	1	pltirr	$⊢ (K \in HL \land X \in V) \to \neg X \underset{˙}{<} X$
4	3	3adant3	$⊢ (K \in HL \land X \in V \land Y \in V) \to \neg X \underset{˙}{<} X$
5		breq2	$⊢ X = Y \to (X \underset{˙}{<} X \leftrightarrow X \underset{˙}{<} Y)$
6	5	notbid	$⊢ X = Y \to (\neg X \underset{˙}{<} X \leftrightarrow \neg X \underset{˙}{<} Y)$
7	4 6	syl5ibcom	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X = Y \to \neg X \underset{˙}{<} Y)$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	8 1	pltle	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X \underset{˙}{<} Y \to X \leq_{K} Y)$
10	8 2	lvolcmp	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X \leq_{K} Y \leftrightarrow X = Y)$
11	9 10	sylibd	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X \underset{˙}{<} Y \to X = Y)$
12	11	necon3ad	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X \neq Y \to \neg X \underset{˙}{<} Y)$
13	7 12	pm2.61dne	$⊢ (K \in HL \land X \in V \land Y \in V) \to \neg X \underset{˙}{<} Y$

Metamath Proof Explorer