This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem islvol4

Description: The predicate "is 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	islvol4	$⊢ (K \in A \land X \in B) \to (X \in V \leftrightarrow \exists y \in P y C X)$

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	1 2 3 4	islvol	$⊢ K \in A \to (X \in V \leftrightarrow (X \in B \land \exists y \in P y C X))$
6	5	baibd	$⊢ (K \in A \land X \in B) \to (X \in V \leftrightarrow \exists y \in P y C X)$