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