lvolnleat

Description: An atom cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012)

	Ref	Expression
Hypotheses	lvolnleat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lvolnleat.a	$⊢ A = Atoms (K)$
	lvolnleat.v	$⊢ V = LVols (K)$
Assertion	lvolnleat	$⊢ (K \in HL \land X \in V \land P \in A) \to \neg X \underset{˙}{\leq} P$

Step	Hyp	Ref	Expression
1		lvolnleat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lvolnleat.a	$⊢ A = Atoms (K)$
3		lvolnleat.v	$⊢ V = LVols (K)$
4		3simpa	$⊢ (K \in HL \land X \in V \land P \in A) \to (K \in HL \land X \in V)$
5		simp3	$⊢ (K \in HL \land X \in V \land P \in A) \to P \in A$
6		eqid	$⊢ join (K) = join (K)$
7	1 6 2 3	lvolnle3at	$⊢ ((K \in HL \land X \in V) \land (P \in A \land P \in A \land P \in A)) \to \neg X \underset{˙}{\leq} ((P join (K) P) join (K) P)$
8	4 5 5 5 7	syl13anc	$⊢ (K \in HL \land X \in V \land P \in A) \to \neg X \underset{˙}{\leq} ((P join (K) P) join (K) P)$
9	6 2	hlatjidm	$⊢ (K \in HL \land P \in A) \to P join (K) P = P$
10	9	3adant2	$⊢ (K \in HL \land X \in V \land P \in A) \to P join (K) P = P$
11	10	oveq1d	$⊢ (K \in HL \land X \in V \land P \in A) \to (P join (K) P) join (K) P = P join (K) P$
12	11 10	eqtrd	$⊢ (K \in HL \land X \in V \land P \in A) \to (P join (K) P) join (K) P = P$
13	12	breq2d	$⊢ (K \in HL \land X \in V \land P \in A) \to (X \underset{˙}{\leq} ((P join (K) P) join (K) P) \leftrightarrow X \underset{˙}{\leq} P)$
14	8 13	mtbid	$⊢ (K \in HL \land X \in V \land P \in A) \to \neg X \underset{˙}{\leq} P$

Metamath Proof Explorer