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 | |- LVols = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LPlanes ` k ) p ( |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | clvol | |- LVols |
|
| 1 | vk | |- k |
|
| 2 | cvv | |- _V |
|
| 3 | vx | |- x |
|
| 4 | cbs | |- Base |
|
| 5 | 1 | cv | |- k |
| 6 | 5 4 | cfv | |- ( Base ` k ) |
| 7 | vp | |- p |
|
| 8 | clpl | |- LPlanes |
|
| 9 | 5 8 | cfv | |- ( LPlanes ` k ) |
| 10 | 7 | cv | |- p |
| 11 | ccvr | |- |
|
| 12 | 5 11 | cfv | |- ( |
| 13 | 3 | cv | |- x |
| 14 | 10 13 12 | wbr | |- p ( |
| 15 | 14 7 9 | wrex | |- E. p e. ( LPlanes ` k ) p ( |
| 16 | 15 3 6 | crab | |- { x e. ( Base ` k ) | E. p e. ( LPlanes ` k ) p ( |
| 17 | 1 2 16 | cmpt | |- ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LPlanes ` k ) p ( |
| 18 | 0 17 | wceq | |- LVols = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LPlanes ` k ) p ( |