Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
cdlemeg47b
Next ⟩
cdlemeg47rv
Metamath Proof Explorer
Ascii
Unicode
Theorem
cdlemeg47b
Description:
TODO: FIX COMMENT.
(Contributed by
NM
, 1-Apr-2013)
Ref
Expression
Hypotheses
cdlemef47.b
⊢
B
=
Base
K
cdlemef47.l
⊢
≤
˙
=
≤
K
cdlemef47.j
⊢
∨
˙
=
join
⁡
K
cdlemef47.m
⊢
∧
˙
=
meet
⁡
K
cdlemef47.a
⊢
A
=
Atoms
⁡
K
cdlemef47.h
⊢
H
=
LHyp
⁡
K
cdlemef47.v
⊢
V
=
Q
∨
˙
P
∧
˙
W
cdlemef47.n
⊢
N
=
v
∨
˙
V
∧
˙
P
∨
˙
Q
∨
˙
v
∧
˙
W
cdlemefs47.o
⊢
O
=
Q
∨
˙
P
∧
˙
N
∨
˙
u
∨
˙
v
∧
˙
W
cdlemef47.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
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
Proof
Step
Hyp
Ref
Expression
1
cdlemef47.b
⊢
B
=
Base
K
2
cdlemef47.l
⊢
≤
˙
=
≤
K
3
cdlemef47.j
⊢
∨
˙
=
join
⁡
K
4
cdlemef47.m
⊢
∧
˙
=
meet
⁡
K
5
cdlemef47.a
⊢
A
=
Atoms
⁡
K
6
cdlemef47.h
⊢
H
=
LHyp
⁡
K
7
cdlemef47.v
⊢
V
=
Q
∨
˙
P
∧
˙
W
8
cdlemef47.n
⊢
N
=
v
∨
˙
V
∧
˙
P
∨
˙
Q
∨
˙
v
∧
˙
W
9
cdlemefs47.o
⊢
O
=
Q
∨
˙
P
∧
˙
N
∨
˙
u
∨
˙
v
∧
˙
W
10
cdlemef47.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
11
3
5
cdleme46f2g2
⊢
K
∈
HL
∧
W
∈
H
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
≠
Q
∧
S
∈
A
∧
¬
S
≤
˙
W
∧
¬
S
≤
˙
P
∨
˙
Q
→
K
∈
HL
∧
W
∈
H
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
≠
P
∧
S
∈
A
∧
¬
S
≤
˙
W
∧
¬
S
≤
˙
Q
∨
˙
P
12
1
2
3
4
5
6
7
8
10
cdlemefr45
⊢
K
∈
HL
∧
W
∈
H
∧
Q
∈
A
∧
¬
Q
≤
˙
W
∧
P
∈
A
∧
¬
P
≤
˙
W
∧
Q
≠
P
∧
S
∈
A
∧
¬
S
≤
˙
W
∧
¬
S
≤
˙
Q
∨
˙
P
→
G
⁡
S
=
⦋
S
/
v
⦌
N
13
11
12
syl
⊢
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