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 = (
	lvolset.p	|- P = ( LPlanes ` K )
	lvolset.v	|- V = ( LVols ` K )
Assertion	islvol4	|- ( ( K e. A /\ X e. B ) -> ( X e. V <-> E. y e. P y C X ) )

Proof

Step	Hyp	Ref	Expression
1		lvolset.b	|- B = ( Base ` K )
2		lvolset.c	|- C = (
3		lvolset.p	|- P = ( LPlanes ` K )
4		lvolset.v	|- V = ( LVols ` K )
5	1 2 3 4	islvol	|- ( K e. A -> ( X e. V <-> ( X e. B /\ E. y e. P y C X ) ) )
6	5	baibd	|- ( ( K e. A /\ X e. B ) -> ( X e. V <-> E. y e. P y C X ) )