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