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 = ( 
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 ) )