Metamath Proof Explorer


Theorem lvolset

Description: The set of 3-dim lattice volumes in a Hilbert lattice. (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 lvolset K A 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 elex K A K V
6 fveq2 k = K Base k = Base K
7 6 1 syl6eqr k = K Base k = B
8 fveq2 k = K LPlanes k = LPlanes K
9 8 3 syl6eqr k = K LPlanes k = P
10 fveq2 k = K k = K
11 10 2 syl6eqr k = K k = C
12 11 breqd k = K y k x y C x
13 9 12 rexeqbidv k = K y LPlanes k y k x y P y C x
14 7 13 rabeqbidv k = K x Base k | y LPlanes k y k x = x B | y P y C x
15 df-lvols LVols = k V x Base k | y LPlanes k y k x
16 1 fvexi B V
17 16 rabex x B | y P y C x V
18 14 15 17 fvmpt K V LVols K = x B | y P y C x
19 4 18 syl5eq K V V = x B | y P y C x
20 5 19 syl K A V = x B | y P y C x