lvolnlelpln

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

	Ref	Expression
Hypotheses	lvolnlelpln.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lvolnlelpln.p	$⊢ P = LPlanes (K)$
	lvolnlelpln.v	$⊢ V = LVols (K)$
Assertion	lvolnlelpln	$⊢ (K \in HL \land X \in V \land Y \in P) \to \neg X \underset{˙}{\leq} Y$

Proof

Step	Hyp	Ref	Expression
1		lvolnlelpln.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lvolnlelpln.p	$⊢ P = LPlanes (K)$
3		lvolnlelpln.v	$⊢ V = LVols (K)$
4		simp3	$⊢ (K \in HL \land X \in V \land Y \in P) \to Y \in P$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ join (K) = join (K)$
7		eqid	$⊢ Atoms (K) = Atoms (K)$
8	5 1 6 7 2	islpln2	$⊢ K \in HL \to (Y \in P \leftrightarrow (Y \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)))$
9	8	3ad2ant1	$⊢ (K \in HL \land X \in V \land Y \in P) \to (Y \in P \leftrightarrow (Y \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)))$
10	4 9	mpbid	$⊢ (K \in HL \land X \in V \land Y \in P) \to (Y \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s))$
11		simp1l1	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to K \in HL$
12		simp1l2	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to X \in V$
13		simp1r	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to q \in Atoms (K)$
14		simp2l	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to r \in Atoms (K)$
15		simp2r	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to s \in Atoms (K)$
16	1 6 7 3	lvolnle3at	$⊢ ((K \in HL \land X \in V) \land (q \in Atoms (K) \land r \in Atoms (K) \land s \in Atoms (K))) \to \neg X \underset{˙}{\leq} ((q join (K) r) join (K) s)$
17	11 12 13 14 15 16	syl23anc	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to \neg X \underset{˙}{\leq} ((q join (K) r) join (K) s)$
18		simp33	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to Y = (q join (K) r) join (K) s$
19	18	breq2d	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\leq} ((q join (K) r) join (K) s))$
20	17 19	mtbird	$⊢ (((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to \neg X \underset{˙}{\leq} Y$
21	20	3exp	$⊢ ((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \to ((r \in Atoms (K) \land s \in Atoms (K)) \to ((q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s) \to \neg X \underset{˙}{\leq} Y))$
22	21	rexlimdvv	$⊢ ((K \in HL \land X \in V \land Y \in P) \land q \in Atoms (K)) \to (\exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s) \to \neg X \underset{˙}{\leq} Y)$
23	22	rexlimdva	$⊢ (K \in HL \land X \in V \land Y \in P) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s) \to \neg X \underset{˙}{\leq} Y)$
24	23	adantld	$⊢ (K \in HL \land X \in V \land Y \in P) \to ((Y \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q join (K) r) \land Y = (q join (K) r) join (K) s)) \to \neg X \underset{˙}{\leq} Y)$
25	10 24	mpd	$⊢ (K \in HL \land X \in V \land Y \in P) \to \neg X \underset{˙}{\leq} Y$

Metamath Proof Explorer

Theorem lvolnlelpln

Proof