This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Norm Megill Construction of a vector space from a Hilbert lattice df-lhyp
Description: Define the set of lattice hyperplanes, which are all lattice elements
covered by 1 (i.e., all co-atoms). We call them "hyperplanes" instead
of "co-atoms" in analogy with projective geometry hyperplanes.
(Contributed by NM , 11-May-2012)
Ref
Expression
Assertion
df-lhyp |- LHyp = ( k e. _V |-> { x e. ( Base ` k ) | x (
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
clh |- LHyp
1
vk |- k
2
cvv |- _V
3
vx |- x
4
cbs |- Base
5
1
cv |- k
6
5 4
cfv |- ( Base ` k )
7
3
cv |- x
8
ccvr |-
9
5 8
cfv |- (
10
cp1 |- 1.
11
5 10
cfv |- ( 1. ` k )
12
7 11 9
wbr |- x (
13
12 3 6
crab |- { x e. ( Base ` k ) | x (
14
1 2 13
cmpt |- ( k e. _V |-> { x e. ( Base ` k ) | x (
15
0 14
wceq |- LHyp = ( k e. _V |-> { x e. ( Base ` k ) | x (