Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of involution and inner product from a Hilbert lattice
mapdrn
Next ⟩
mapdunirnN
Metamath Proof Explorer
Ascii
Unicode
Theorem
mapdrn
Description:
Range of the map defined by
df-mapd
.
(Contributed by
NM
, 12-Mar-2015)
Ref
Expression
Hypotheses
mapdrn.h
⊢
H
=
LHyp
⁡
K
mapdrn.o
⊢
O
=
ocH
⁡
K
⁡
W
mapdrn.m
⊢
M
=
mapd
⁡
K
⁡
W
mapdrn.u
⊢
U
=
DVecH
⁡
K
⁡
W
mapdrn.f
⊢
F
=
LFnl
⁡
U
mapdrn.l
⊢
L
=
LKer
⁡
U
mapdrn.d
⊢
D
=
LDual
⁡
U
mapdrn.t
⊢
T
=
LSubSp
⁡
D
mapdrn.c
⊢
C
=
g
∈
F
|
O
⁡
O
⁡
L
⁡
g
=
L
⁡
g
mapdrn.k
⊢
φ
→
K
∈
HL
∧
W
∈
H
Assertion
mapdrn
⊢
φ
→
ran
⁡
M
=
T
∩
𝒫
C
Proof
Step
Hyp
Ref
Expression
1
mapdrn.h
⊢
H
=
LHyp
⁡
K
2
mapdrn.o
⊢
O
=
ocH
⁡
K
⁡
W
3
mapdrn.m
⊢
M
=
mapd
⁡
K
⁡
W
4
mapdrn.u
⊢
U
=
DVecH
⁡
K
⁡
W
5
mapdrn.f
⊢
F
=
LFnl
⁡
U
6
mapdrn.l
⊢
L
=
LKer
⁡
U
7
mapdrn.d
⊢
D
=
LDual
⁡
U
8
mapdrn.t
⊢
T
=
LSubSp
⁡
D
9
mapdrn.c
⊢
C
=
g
∈
F
|
O
⁡
O
⁡
L
⁡
g
=
L
⁡
g
10
mapdrn.k
⊢
φ
→
K
∈
HL
∧
W
∈
H
11
eqid
⊢
LSubSp
⁡
U
=
LSubSp
⁡
U
12
1
2
3
4
11
5
6
7
8
9
10
mapd1o
⊢
φ
→
M
:
LSubSp
⁡
U
⟶
1-1 onto
T
∩
𝒫
C
13
f1ofo
⊢
M
:
LSubSp
⁡
U
⟶
1-1 onto
T
∩
𝒫
C
→
M
:
LSubSp
⁡
U
⟶
onto
T
∩
𝒫
C
14
forn
⊢
M
:
LSubSp
⁡
U
⟶
onto
T
∩
𝒫
C
→
ran
⁡
M
=
T
∩
𝒫
C
15
12
13
14
3syl
⊢
φ
→
ran
⁡
M
=
T
∩
𝒫
C