Description: Define the set of all "lattice planes" (lattice elements which cover a line) in a Hilbert lattice k , in other words all elements of height 3 (or lattice dimension 3 or projective dimension 2). (Contributed by NM, 16-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | df-lplanes | |- LPlanes = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | clpl | |- LPlanes |
|
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 | clln | |- LLines |
|
9 | 5 8 | cfv | |- ( LLines ` 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. ( LLines ` k ) p ( |
16 | 15 3 6 | crab | |- { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( |
17 | 1 2 16 | cmpt | |- ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( |
18 | 0 17 | wceq | |- LPlanes = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( |