Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
tendoi2
Next ⟩
tendoicl
Metamath Proof Explorer
Ascii
Unicode
Theorem
tendoi2
Description:
Value of additive 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
tendoi2
⊢
S
∈
E
∧
F
∈
T
→
I
⁡
S
⁡
F
=
S
⁡
F
-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
1
2
tendoi
⊢
S
∈
E
→
I
⁡
S
=
g
∈
T
⟼
S
⁡
g
-1
4
3
adantr
⊢
S
∈
E
∧
F
∈
T
→
I
⁡
S
=
g
∈
T
⟼
S
⁡
g
-1
5
fveq2
⊢
g
=
F
→
S
⁡
g
=
S
⁡
F
6
5
cnveqd
⊢
g
=
F
→
S
⁡
g
-1
=
S
⁡
F
-1
7
6
adantl
⊢
S
∈
E
∧
F
∈
T
∧
g
=
F
→
S
⁡
g
-1
=
S
⁡
F
-1
8
simpr
⊢
S
∈
E
∧
F
∈
T
→
F
∈
T
9
fvex
⊢
S
⁡
F
∈
V
10
9
cnvex
⊢
S
⁡
F
-1
∈
V
11
10
a1i
⊢
S
∈
E
∧
F
∈
T
→
S
⁡
F
-1
∈
V
12
4
7
8
11
fvmptd
⊢
S
∈
E
∧
F
∈
T
→
I
⁡
S
⁡
F
=
S
⁡
F
-1