Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
dibfna
Next ⟩
dibdiadm
Metamath Proof Explorer
Ascii
Unicode
Theorem
dibfna
Description:
Functionality and domain of the partial isomorphism B.
(Contributed by
NM
, 17-Jan-2014)
Ref
Expression
Hypotheses
dibfna.h
⊢
H
=
LHyp
⁡
K
dibfna.j
⊢
J
=
DIsoA
⁡
K
⁡
W
dibfna.i
⊢
I
=
DIsoB
⁡
K
⁡
W
Assertion
dibfna
⊢
K
∈
V
∧
W
∈
H
→
I
Fn
dom
⁡
J
Proof
Step
Hyp
Ref
Expression
1
dibfna.h
⊢
H
=
LHyp
⁡
K
2
dibfna.j
⊢
J
=
DIsoA
⁡
K
⁡
W
3
dibfna.i
⊢
I
=
DIsoB
⁡
K
⁡
W
4
fvex
⊢
J
⁡
y
∈
V
5
snex
⊢
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
∈
V
6
4
5
xpex
⊢
J
⁡
y
×
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
∈
V
7
eqid
⊢
y
∈
dom
⁡
J
⟼
J
⁡
y
×
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
=
y
∈
dom
⁡
J
⟼
J
⁡
y
×
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
8
6
7
fnmpti
⊢
y
∈
dom
⁡
J
⟼
J
⁡
y
×
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
Fn
dom
⁡
J
9
eqid
⊢
Base
K
=
Base
K
10
eqid
⊢
LTrn
⁡
K
⁡
W
=
LTrn
⁡
K
⁡
W
11
eqid
⊢
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
=
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
12
9
1
10
11
2
3
dibfval
⊢
K
∈
V
∧
W
∈
H
→
I
=
y
∈
dom
⁡
J
⟼
J
⁡
y
×
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
13
12
fneq1d
⊢
K
∈
V
∧
W
∈
H
→
I
Fn
dom
⁡
J
↔
y
∈
dom
⁡
J
⟼
J
⁡
y
×
f
∈
LTrn
⁡
K
⁡
W
⟼
I
↾
Base
K
Fn
dom
⁡
J
14
8
13
mpbiri
⊢
K
∈
V
∧
W
∈
H
→
I
Fn
dom
⁡
J