lvolnlelln

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

	Ref	Expression
Hypotheses	lvolnlelln.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lvolnlelln.n	$⊢ N = LLines (K)$
	lvolnlelln.v	$⊢ V = LVols (K)$
Assertion	lvolnlelln	$⊢ (K \in HL \land X \in V \land Y \in N) \to \neg X \underset{˙}{\leq} Y$

Proof

Step	Hyp	Ref	Expression
1		lvolnlelln.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lvolnlelln.n	$⊢ N = LLines (K)$
3		lvolnlelln.v	$⊢ V = LVols (K)$
4		simp3	$⊢ (K \in HL \land X \in V \land Y \in N) \to Y \in N$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ join (K) = join (K)$
7		eqid	$⊢ Atoms (K) = Atoms (K)$
8	5 6 7 2	islln2	$⊢ K \in HL \to (Y \in N \leftrightarrow (Y \in {Base}_{K} \land \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land Y = p join (K) q)))$
9	8	3ad2ant1	$⊢ (K \in HL \land X \in V \land Y \in N) \to (Y \in N \leftrightarrow (Y \in {Base}_{K} \land \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land Y = p join (K) q)))$
10	4 9	mpbid	$⊢ (K \in HL \land X \in V \land Y \in N) \to (Y \in {Base}_{K} \land \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land Y = p join (K) q))$
11		simp11	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to K \in HL$
12		simp12	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to X \in V$
13		simp2l	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to p \in Atoms (K)$
14		simp2r	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to q \in Atoms (K)$
15	1 6 7 3	lvolnle3at	$⊢ ((K \in HL \land X \in V) \land (p \in Atoms (K) \land p \in Atoms (K) \land q \in Atoms (K))) \to \neg X \underset{˙}{\leq} ((p join (K) p) join (K) q)$
16	11 12 13 13 14 15	syl23anc	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to \neg X \underset{˙}{\leq} ((p join (K) p) join (K) q)$
17		simp3r	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to Y = p join (K) q$
18	6 7	hlatjidm	$⊢ (K \in HL \land p \in Atoms (K)) \to p join (K) p = p$
19	11 13 18	syl2anc	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to p join (K) p = p$
20	19	oveq1d	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to (p join (K) p) join (K) q = p join (K) q$
21	17 20	eqtr4d	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to Y = (p join (K) p) join (K) q$
22	21	breq2d	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\leq} ((p join (K) p) join (K) q))$
23	16 22	mtbird	$⊢ ((K \in HL \land X \in V \land Y \in N) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land Y = p join (K) q)) \to \neg X \underset{˙}{\leq} Y$
24	23	3exp	$⊢ (K \in HL \land X \in V \land Y \in N) \to ((p \in Atoms (K) \land q \in Atoms (K)) \to ((p \neq q \land Y = p join (K) q) \to \neg X \underset{˙}{\leq} Y))$
25	24	rexlimdvv	$⊢ (K \in HL \land X \in V \land Y \in N) \to (\exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land Y = p join (K) q) \to \neg X \underset{˙}{\leq} Y)$
26	25	adantld	$⊢ (K \in HL \land X \in V \land Y \in N) \to ((Y \in {Base}_{K} \land \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land Y = p join (K) q)) \to \neg X \underset{˙}{\leq} Y)$
27	10 26	mpd	$⊢ (K \in HL \land X \in V \land Y \in N) \to \neg X \underset{˙}{\leq} Y$

Metamath Proof Explorer

Theorem lvolnlelln

Proof