Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
tendoi
Next ⟩
tendoi2
Metamath Proof Explorer
Ascii
Unicode
Theorem
tendoi
Description:
Value of inverse endomorphism.
(Contributed by
NM
, 12-Jun-2013)
Ref
Expression
Hypotheses
tendoi.i
⊢
I
=
s
∈
E
⟼
f
∈
T
⟼
s
⁡
f
-1
tendoi.t
⊢
T
=
LTrn
⁡
K
⁡
W
Assertion
tendoi
⊢
S
∈
E
→
I
⁡
S
=
g
∈
T
⟼
S
⁡
g
-1
Proof
Step
Hyp
Ref
Expression
1
tendoi.i
⊢
I
=
s
∈
E
⟼
f
∈
T
⟼
s
⁡
f
-1
2
tendoi.t
⊢
T
=
LTrn
⁡
K
⁡
W
3
fveq1
⊢
u
=
S
→
u
⁡
g
=
S
⁡
g
4
3
cnveqd
⊢
u
=
S
→
u
⁡
g
-1
=
S
⁡
g
-1
5
4
mpteq2dv
⊢
u
=
S
→
g
∈
T
⟼
u
⁡
g
-1
=
g
∈
T
⟼
S
⁡
g
-1
6
1
tendoicbv
⊢
I
=
u
∈
E
⟼
g
∈
T
⟼
u
⁡
g
-1
7
5
6
2
mptfvmpt
⊢
S
∈
E
→
I
⁡
S
=
g
∈
T
⟼
S
⁡
g
-1