Metamath Proof Explorer


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