Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
tendopl
Next ⟩
tendopl2
Metamath Proof Explorer
Ascii
Unicode
Theorem
tendopl
Description:
Value of endomorphism sum operation.
(Contributed by
NM
, 10-Jun-2013)
Ref
Expression
Hypotheses
tendoplcbv.p
⊢
P
=
s
∈
E
,
t
∈
E
⟼
f
∈
T
⟼
s
⁡
f
∘
t
⁡
f
tendopl2.t
⊢
T
=
LTrn
⁡
K
⁡
W
Assertion
tendopl
⊢
U
∈
E
∧
V
∈
E
→
U
P
V
=
g
∈
T
⟼
U
⁡
g
∘
V
⁡
g
Proof
Step
Hyp
Ref
Expression
1
tendoplcbv.p
⊢
P
=
s
∈
E
,
t
∈
E
⟼
f
∈
T
⟼
s
⁡
f
∘
t
⁡
f
2
tendopl2.t
⊢
T
=
LTrn
⁡
K
⁡
W
3
fveq1
⊢
u
=
U
→
u
⁡
g
=
U
⁡
g
4
3
coeq1d
⊢
u
=
U
→
u
⁡
g
∘
v
⁡
g
=
U
⁡
g
∘
v
⁡
g
5
4
mpteq2dv
⊢
u
=
U
→
g
∈
T
⟼
u
⁡
g
∘
v
⁡
g
=
g
∈
T
⟼
U
⁡
g
∘
v
⁡
g
6
fveq1
⊢
v
=
V
→
v
⁡
g
=
V
⁡
g
7
6
coeq2d
⊢
v
=
V
→
U
⁡
g
∘
v
⁡
g
=
U
⁡
g
∘
V
⁡
g
8
7
mpteq2dv
⊢
v
=
V
→
g
∈
T
⟼
U
⁡
g
∘
v
⁡
g
=
g
∈
T
⟼
U
⁡
g
∘
V
⁡
g
9
1
tendoplcbv
⊢
P
=
u
∈
E
,
v
∈
E
⟼
g
∈
T
⟼
u
⁡
g
∘
v
⁡
g
10
2
fvexi
⊢
T
∈
V
11
10
mptex
⊢
g
∈
T
⟼
U
⁡
g
∘
V
⁡
g
∈
V
12
5
8
9
11
ovmpo
⊢
U
∈
E
∧
V
∈
E
→
U
P
V
=
g
∈
T
⟼
U
⁡
g
∘
V
⁡
g