Metamath Proof Explorer


Theorem islvol

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 islvol K A X V X B y P y C X

Proof

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 lvolset K A V = x B | y P y C x
6 5 eleq2d K A X V X x B | y P y C x
7 breq2 x = X y C x y C X
8 7 rexbidv x = X y P y C x y P y C X
9 8 elrab X x B | y P y C x X B y P y C X
10 6 9 bitrdi K A X V X B y P y C X