Definition df-lvols

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)

	Ref	Expression
Assertion	df-lvols	$$⊢\mathrm{LVols}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{LPlanes}\left(k\right)p{⋖}_{k}x\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clvol	$$class\mathrm{LVols}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class{\mathrm{Base}}_k$$
7		vp	$$setvarp$$
8		clpl	$$class\mathrm{LPlanes}$$
9	5 8	cfv	$$class\mathrm{LPlanes}\left(k\right)$$
10	7	cv	$$setvarp$$
11		ccvr	$$class⋖$$
12	5 11	cfv	$$class{⋖}_k$$
13	3	cv	$$setvarx$$
14	10 13 12	wbr	$$wffp{⋖}_{k}x$$
15	14 7 9	wrex	$$wff\exists p\in \mathrm{LPlanes}\left(k\right)p{⋖}_{k}x$$
16	15 3 6	crab	$$class\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{LPlanes}\left(k\right)p{⋖}_{k}x\right\}$$
17	1 2 16	cmpt	$$class\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{LPlanes}\left(k\right)p{⋖}_{k}x\right\}\right)$$
18	0 17	wceq	$$wff\mathrm{LVols}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{LPlanes}\left(k\right)p{⋖}_{k}x\right\}\right)$$