This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = (
lvolset.p 
|- P = ( LPlanes ` K )
lvolset.v 
|- V = ( LVols ` K )
Assertion lvolset 
|- ( K e. A -> V = { x e. B | 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 elex 
 |-  ( K e. A -> K e. _V )
6 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
7 6 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
8 fveq2 
 |-  ( k = K -> ( LPlanes ` k ) = ( LPlanes ` K ) )
9 8 3 eqtr4di 
 |-  ( k = K -> ( LPlanes ` k ) = P )
10 fveq2 
 |-  ( k = K -> (
11 10 2 eqtr4di 
 |-  ( k = K -> (
12 11 breqd 
 |-  ( k = K -> ( y (  y C x ) )
13 9 12 rexeqbidv 
 |-  ( k = K -> ( E. y e. ( LPlanes ` k ) y (  E. y e. P y C x ) )
14 7 13 rabeqbidv 
 |-  ( k = K -> { x e. ( Base ` k ) | E. y e. ( LPlanes ` k ) y (
15 df-lvols 
 |-  LVols = ( k e. _V |-> { x e. ( Base ` k ) | E. y e. ( LPlanes ` k ) y (
16 1 fvexi 
 |-  B e. _V
17 16 rabex 
 |-  { x e. B | E. y e. P y C x } e. _V
18 14 15 17 fvmpt 
 |-  ( K e. _V -> ( LVols ` K ) = { x e. B | E. y e. P y C x } )
19 4 18 eqtrid 
 |-  ( K e. _V -> V = { x e. B | E. y e. P y C x } )
20 5 19 syl 
 |-  ( K e. A -> V = { x e. B | E. y e. P y C x } )