Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
cdlemeg46bOLDN
Next ⟩
cdlemeg46c
Metamath Proof Explorer
Ascii
Unicode
Theorem
cdlemeg46bOLDN
Description:
TODO FIX COMMENT.
(Contributed by
NM
, 1-Apr-2013)
(New usage is discouraged.)
Ref
Expression
Hypotheses
cdlemef46g.b
⊢
B
=
Base
K
cdlemef46g.l
⊢
≤
˙
=
≤
K
cdlemef46g.j
⊢
∨
˙
=
join
⁡
K
cdlemef46g.m
⊢
∧
˙
=
meet
⁡
K
cdlemef46g.a
⊢
A
=
Atoms
⁡
K
cdlemef46g.h
⊢
H
=
LHyp
⁡
K
cdlemef46g.u
⊢
U
=
P
∨
˙
Q
∧
˙
W
cdlemef46g.d
⊢
D
=
t
∨
˙
U
∧
˙
Q
∨
˙
P
∨
˙
t
∧
˙
W
cdlemefs46g.e
⊢
E
=
P
∨
˙
Q
∧
˙
D
∨
˙
s
∨
˙
t
∧
˙
W
cdlemef46g.f
⊢
F
=
x
∈
B
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
x
∧
˙
W
=
x
→
z
=
if
s
≤
˙
P
∨
˙
Q
ι
y
∈
B
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
∨
˙
Q
→
y
=
E
⦋
s
/
t
⦌
D
∨
˙
x
∧
˙
W
x
cdlemef46.v
⊢
V
=
Q
∨
˙
P
∧
˙
W
cdlemef46.n
⊢
N
=
v
∨
˙
V
∧
˙
P
∨
˙
Q
∨
˙
v
∧
˙
W
cdlemefs46.o
⊢
O
=
Q
∨
˙
P
∧
˙
N
∨
˙
u
∨
˙
v
∧
˙
W
cdlemef46.g
⊢
G
=
a
∈
B
⟼
if
Q
≠
P
∧
¬
a
≤
˙
W
ι
c
∈
B
|
∀
u
∈
A
¬
u
≤
˙
W
∧
u
∨
˙
a
∧
˙
W
=
a
→
c
=
if
u
≤
˙
Q
∨
˙
P
ι
b
∈
B
|
∀
v
∈
A
¬
v
≤
˙
W
∧
¬
v
≤
˙
Q
∨
˙
P
→
b
=
O
⦋
u
/
v
⦌
N
∨
˙
a
∧
˙
W
a
Assertion
cdlemeg46bOLDN
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
≠
Q
∧
S
∈
A
∧
¬
S
≤
˙
W
∧
¬
S
≤
˙
P
∨
˙
Q
→
G
⁡
S
=
⦋
S
/
v
⦌
N
Proof
Step
Hyp
Ref
Expression
1
cdlemef46g.b
⊢
B
=
Base
K
2
cdlemef46g.l
⊢
≤
˙
=
≤
K
3
cdlemef46g.j
⊢
∨
˙
=
join
⁡
K
4
cdlemef46g.m
⊢
∧
˙
=
meet
⁡
K
5
cdlemef46g.a
⊢
A
=
Atoms
⁡
K
6
cdlemef46g.h
⊢
H
=
LHyp
⁡
K
7
cdlemef46g.u
⊢
U
=
P
∨
˙
Q
∧
˙
W
8
cdlemef46g.d
⊢
D
=
t
∨
˙
U
∧
˙
Q
∨
˙
P
∨
˙
t
∧
˙
W
9
cdlemefs46g.e
⊢
E
=
P
∨
˙
Q
∧
˙
D
∨
˙
s
∨
˙
t
∧
˙
W
10
cdlemef46g.f
⊢
F
=
x
∈
B
⟼
if
P
≠
Q
∧
¬
x
≤
˙
W
ι
z
∈
B
|
∀
s
∈
A
¬
s
≤
˙
W
∧
s
∨
˙
x
∧
˙
W
=
x
→
z
=
if
s
≤
˙
P
∨
˙
Q
ι
y
∈
B
|
∀
t
∈
A
¬
t
≤
˙
W
∧
¬
t
≤
˙
P
∨
˙
Q
→
y
=
E
⦋
s
/
t
⦌
D
∨
˙
x
∧
˙
W
x
11
cdlemef46.v
⊢
V
=
Q
∨
˙
P
∧
˙
W
12
cdlemef46.n
⊢
N
=
v
∨
˙
V
∧
˙
P
∨
˙
Q
∨
˙
v
∧
˙
W
13
cdlemefs46.o
⊢
O
=
Q
∨
˙
P
∧
˙
N
∨
˙
u
∨
˙
v
∧
˙
W
14
cdlemef46.g
⊢
G
=
a
∈
B
⟼
if
Q
≠
P
∧
¬
a
≤
˙
W
ι
c
∈
B
|
∀
u
∈
A
¬
u
≤
˙
W
∧
u
∨
˙
a
∧
˙
W
=
a
→
c
=
if
u
≤
˙
Q
∨
˙
P
ι
b
∈
B
|
∀
v
∈
A
¬
v
≤
˙
W
∧
¬
v
≤
˙
Q
∨
˙
P
→
b
=
O
⦋
u
/
v
⦌
N
∨
˙
a
∧
˙
W
a
15
1
2
3
4
5
6
11
12
13
14
cdlemeg47b
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
≠
Q
∧
S
∈
A
∧
¬
S
≤
˙
W
∧
¬
S
≤
˙
P
∨
˙
Q
→
G
⁡
S
=
⦋
S
/
v
⦌
N