Theorem tendopl2

Description: Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013)

	Ref	Expression
Hypotheses	tendoplcbv.p	$$⊢P=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
	tendopl2.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	tendopl2	$$⊢\left(U\in E\wedge V\in E\wedge F\in T\right)\to \left(UPV\right)\left(F\right)=U\left(F\right)\circ V\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		tendoplcbv.p	$$⊢P=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
2		tendopl2.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3	1 2	tendopl	$$⊢\left(U\in E\wedge V\in E\right)\to UPV=\left(g\in T⟼U\left(g\right)\circ V\left(g\right)\right)$$
4	3	3adant3	$$⊢\left(U\in E\wedge V\in E\wedge F\in T\right)\to UPV=\left(g\in T⟼U\left(g\right)\circ V\left(g\right)\right)$$
5		fveq2	$$⊢g=F\to U\left(g\right)=U\left(F\right)$$
6		fveq2	$$⊢g=F\to V\left(g\right)=V\left(F\right)$$
7	5 6	coeq12d	$$⊢g=F\to U\left(g\right)\circ V\left(g\right)=U\left(F\right)\circ V\left(F\right)$$
8	7	adantl	$$⊢\left(\left(U\in E\wedge V\in E\wedge F\in T\right)\wedge g=F\right)\to U\left(g\right)\circ V\left(g\right)=U\left(F\right)\circ V\left(F\right)$$
9		simp3	$$⊢\left(U\in E\wedge V\in E\wedge F\in T\right)\to F\in T$$
10		fvex	$$⊢U\left(F\right)\in \mathrm{V}$$
11		fvex	$$⊢V\left(F\right)\in \mathrm{V}$$
12	10 11	coex	$$⊢U\left(F\right)\circ V\left(F\right)\in \mathrm{V}$$
13	12	a1i	$$⊢\left(U\in E\wedge V\in E\wedge F\in T\right)\to U\left(F\right)\circ V\left(F\right)\in \mathrm{V}$$
14	4 8 9 13	fvmptd	$$⊢\left(U\in E\wedge V\in E\wedge F\in T\right)\to \left(UPV\right)\left(F\right)=U\left(F\right)\circ V\left(F\right)$$