Definition df-lvols 34786

Description: Define the set of all 3-dimensional "lattice volumes" (lattice elements which cover a plane) in a Hilbert lattice k, in other words all elements of height 4 (or lattice dimension 4 or projective dimension 3). (Contributed by NM, 1-Jul-2012.)

Assertion

Ref	Expression
df-lvols	|- LVols = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LPlanes ` k ) p ( <o ` k ) x } )

Distinct variable group:   k, p, x

Detailed syntax breakdown of Definition df-lvols

Step	Hyp	Ref	Expression
1		clvol 34779	. 2 class LVols
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vp	. . . . . . 7 setvar p
5	4	cv 1482	. . . . . 6 class p
6		vx	. . . . . . 7 setvar x
7	6	cv 1482	. . . . . 6 class x
8	2	cv 1482	. . . . . . 7 class k
9		ccvr 34549	. . . . . . 7 class <o
10	8, 9	cfv 5888	. . . . . 6 class ( <o ` k )
11	5, 7, 10	wbr 4653	. . . . 5 wff p ( <o ` k ) x
12		clpl 34778	. . . . . 6 class LPlanes
13	8, 12	cfv 5888	. . . . 5 class ( LPlanes ` k )
14	11, 4, 13	wrex 2913	. . . 4 wff E. p e. ( LPlanes ` k ) p ( <o ` k ) x
15		cbs 15857	. . . . 5 class Base
16	8, 15	cfv 5888	. . . 4 class ( Base ` k )
17	14, 6, 16	crab 2916	. . 3 class { x e. ( Base ` k ) | E. p e. ( LPlanes ` k ) p ( <o ` k ) x }
18	2, 3, 17	cmpt 4729	. 2 class ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LPlanes ` k ) p ( <o ` k ) x } )
19	1, 18	wceq 1483	1 wff LVols = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LPlanes ` k ) p ( <o ` k ) x } )

This definition is referenced by:  lvolset  34858