Theorem islvol

Description: The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Hypotheses	lvolset.b	$$⊢B={\mathrm{Base}}_K$$
	lvolset.c	$$⊢C={⋖}_K$$
	lvolset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
	lvolset.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	islvol	$$⊢K\in A\to \left(X\in V\leftrightarrow \left(X\in B\wedge \exists y\in PyCX\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lvolset.b	$$⊢B={\mathrm{Base}}_K$$
2		lvolset.c	$$⊢C={⋖}_K$$
3		lvolset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
4		lvolset.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
5	1 2 3 4	lvolset	$$⊢K\in A\to V=\left\{x\in B|\exists y\in PyCx\right\}$$
6	5	eleq2d	$$⊢K\in A\to \left(X\in V\leftrightarrow X\in \left\{x\in B|\exists y\in PyCx\right\}\right)$$
7		breq2	$$⊢x=X\to \left(yCx\leftrightarrow yCX\right)$$
8	7	rexbidv	$$⊢x=X\to \left(\exists y\in PyCx\leftrightarrow \exists y\in PyCX\right)$$
9	8	elrab	$$⊢X\in \left\{x\in B|\exists y\in PyCx\right\}\leftrightarrow \left(X\in B\wedge \exists y\in PyCX\right)$$
10	6 9	bitrdi	$$⊢K\in A\to \left(X\in V\leftrightarrow \left(X\in B\wedge \exists y\in PyCX\right)\right)$$