Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
cdlemk40t
Next ⟩
cdlemk40f
Metamath Proof Explorer
Ascii
Unicode
Theorem
cdlemk40t
Description:
TODO: fix comment.
(Contributed by
NM
, 31-Jul-2013)
Ref
Expression
Hypotheses
cdlemk40.x
⊢
X
=
ι
z
∈
T
|
φ
cdlemk40.u
⊢
U
=
g
∈
T
⟼
if
F
=
N
g
X
Assertion
cdlemk40t
⊢
F
=
N
∧
G
∈
T
→
U
⁡
G
=
G
Proof
Step
Hyp
Ref
Expression
1
cdlemk40.x
⊢
X
=
ι
z
∈
T
|
φ
2
cdlemk40.u
⊢
U
=
g
∈
T
⟼
if
F
=
N
g
X
3
1
2
cdlemk40
⊢
G
∈
T
→
U
⁡
G
=
if
F
=
N
G
⦋
G
/
g
⦌
X
4
iftrue
⊢
F
=
N
→
if
F
=
N
G
⦋
G
/
g
⦌
X
=
G
5
3
4
sylan9eqr
⊢
F
=
N
∧
G
∈
T
→
U
⁡
G
=
G