lvoli

Description: Condition implying a 3-dim lattice volume. (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Hypotheses	lvolset.b	$⊢ B = {Base}_{K}$
	lvolset.c	$⊢ C = ⋖_{K}$
	lvolset.p	$⊢ P = LPlanes (K)$
	lvolset.v	$⊢ V = LVols (K)$
Assertion	lvoli	$⊢ ((K \in D \land Y \in B \land X \in P) \land X C Y) \to Y \in V$

Step	Hyp	Ref	Expression
1		lvolset.b	$⊢ B = {Base}_{K}$
2		lvolset.c	$⊢ C = ⋖_{K}$
3		lvolset.p	$⊢ P = LPlanes (K)$
4		lvolset.v	$⊢ V = LVols (K)$
5		simpl2	$⊢ ((K \in D \land Y \in B \land X \in P) \land X C Y) \to Y \in B$
6		breq1	$⊢ x = X \to (x C Y \leftrightarrow X C Y)$
7	6	rspcev	$⊢ (X \in P \land X C Y) \to \exists x \in P x C Y$
8	7	3ad2antl3	$⊢ ((K \in D \land Y \in B \land X \in P) \land X C Y) \to \exists x \in P x C Y$
9		simpl1	$⊢ ((K \in D \land Y \in B \land X \in P) \land X C Y) \to K \in D$
10	1 2 3 4	islvol	$⊢ K \in D \to (Y \in V \leftrightarrow (Y \in B \land \exists x \in P x C Y))$
11	9 10	syl	$⊢ ((K \in D \land Y \in B \land X \in P) \land X C Y) \to (Y \in V \leftrightarrow (Y \in B \land \exists x \in P x C Y))$
12	5 8 11	mpbir2and	$⊢ ((K \in D \land Y \in B \land X \in P) \land X C Y) \to Y \in V$

Metamath Proof Explorer