Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
dihsslss
Next ⟩
dihrnlss
Metamath Proof Explorer
Ascii
Unicode
Theorem
dihsslss
Description:
The isomorphism H maps to subspaces.
(Contributed by
NM
, 14-Mar-2014)
Ref
Expression
Hypotheses
dihsslss.h
⊢
H
=
LHyp
⁡
K
dihsslss.u
⊢
U
=
DVecH
⁡
K
⁡
W
dihsslss.i
⊢
I
=
DIsoH
⁡
K
⁡
W
dihsslss.s
⊢
S
=
LSubSp
⁡
U
Assertion
dihsslss
⊢
K
∈
HL
∧
W
∈
H
→
ran
⁡
I
⊆
S
Proof
Step
Hyp
Ref
Expression
1
dihsslss.h
⊢
H
=
LHyp
⁡
K
2
dihsslss.u
⊢
U
=
DVecH
⁡
K
⁡
W
3
dihsslss.i
⊢
I
=
DIsoH
⁡
K
⁡
W
4
dihsslss.s
⊢
S
=
LSubSp
⁡
U
5
1
3
dihcnvid2
⊢
K
∈
HL
∧
W
∈
H
∧
x
∈
ran
⁡
I
→
I
⁡
I
-1
⁡
x
=
x
6
eqid
⊢
Base
K
=
Base
K
7
6
1
3
dihcnvcl
⊢
K
∈
HL
∧
W
∈
H
∧
x
∈
ran
⁡
I
→
I
-1
⁡
x
∈
Base
K
8
6
1
3
2
4
dihlss
⊢
K
∈
HL
∧
W
∈
H
∧
I
-1
⁡
x
∈
Base
K
→
I
⁡
I
-1
⁡
x
∈
S
9
7
8
syldan
⊢
K
∈
HL
∧
W
∈
H
∧
x
∈
ran
⁡
I
→
I
⁡
I
-1
⁡
x
∈
S
10
5
9
eqeltrrd
⊢
K
∈
HL
∧
W
∈
H
∧
x
∈
ran
⁡
I
→
x
∈
S
11
10
ex
⊢
K
∈
HL
∧
W
∈
H
→
x
∈
ran
⁡
I
→
x
∈
S
12
11
ssrdv
⊢
K
∈
HL
∧
W
∈
H
→
ran
⁡
I
⊆
S