Theorem tendovalco

Description: Value of composition of translations in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013)

	Ref	Expression
Hypotheses	tendof.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	tendof.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	tendof.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
Assertion	tendovalco	$$⊢\left(\left(K\in V\wedge W\in H\wedge S\in E\right)\wedge \left(F\in T\wedge G\in T\right)\right)\to S\left(F\circ G\right)=S\left(F\right)\circ S\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		tendof.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		tendof.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		tendof.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		eqid	$$⊢{\le }_K={\le }_K$$
5		eqid	$$⊢\mathrm{trL}\left(K\right)\left(W\right)=\mathrm{trL}\left(K\right)\left(W\right)$$
6	4 1 2 5 3	istendo	$$⊢\left(K\in V\wedge W\in H\right)\to \left(S\in E\leftrightarrow \left(S:T⟶T\wedge \forall f\in T\forall g\in TS\left(f\circ g\right)=S\left(f\right)\circ S\left(g\right)\wedge \forall f\in T\mathrm{trL}\left(K\right)\left(W\right)\left(S\left(f\right)\right){\le }_K\mathrm{trL}\left(K\right)\left(W\right)\left(f\right)\right)\right)$$
7		coeq1	$$⊢f=F\to f\circ g=F\circ g$$
8	7	fveq2d	$$⊢f=F\to S\left(f\circ g\right)=S\left(F\circ g\right)$$
9		fveq2	$$⊢f=F\to S\left(f\right)=S\left(F\right)$$
10	9	coeq1d	$$⊢f=F\to S\left(f\right)\circ S\left(g\right)=S\left(F\right)\circ S\left(g\right)$$
11	8 10	eqeq12d	$$⊢f=F\to \left(S\left(f\circ g\right)=S\left(f\right)\circ S\left(g\right)\leftrightarrow S\left(F\circ g\right)=S\left(F\right)\circ S\left(g\right)\right)$$
12		coeq2	$$⊢g=G\to F\circ g=F\circ G$$
13	12	fveq2d	$$⊢g=G\to S\left(F\circ g\right)=S\left(F\circ G\right)$$
14		fveq2	$$⊢g=G\to S\left(g\right)=S\left(G\right)$$
15	14	coeq2d	$$⊢g=G\to S\left(F\right)\circ S\left(g\right)=S\left(F\right)\circ S\left(G\right)$$
16	13 15	eqeq12d	$$⊢g=G\to \left(S\left(F\circ g\right)=S\left(F\right)\circ S\left(g\right)\leftrightarrow S\left(F\circ G\right)=S\left(F\right)\circ S\left(G\right)\right)$$
17	11 16	rspc2v	$$⊢\left(F\in T\wedge G\in T\right)\to \left(\forall f\in T\forall g\in TS\left(f\circ g\right)=S\left(f\right)\circ S\left(g\right)\to S\left(F\circ G\right)=S\left(F\right)\circ S\left(G\right)\right)$$
18	17	com12	$$⊢\forall f\in T\forall g\in TS\left(f\circ g\right)=S\left(f\right)\circ S\left(g\right)\to \left(\left(F\in T\wedge G\in T\right)\to S\left(F\circ G\right)=S\left(F\right)\circ S\left(G\right)\right)$$
19	18	3ad2ant2	$$⊢\left(S:T⟶T\wedge \forall f\in T\forall g\in TS\left(f\circ g\right)=S\left(f\right)\circ S\left(g\right)\wedge \forall f\in T\mathrm{trL}\left(K\right)\left(W\right)\left(S\left(f\right)\right){\le }_K\mathrm{trL}\left(K\right)\left(W\right)\left(f\right)\right)\to \left(\left(F\in T\wedge G\in T\right)\to S\left(F\circ G\right)=S\left(F\right)\circ S\left(G\right)\right)$$
20	6 19	syl6bi	$$⊢\left(K\in V\wedge W\in H\right)\to \left(S\in E\to \left(\left(F\in T\wedge G\in T\right)\to S\left(F\circ G\right)=S\left(F\right)\circ S\left(G\right)\right)\right)$$
21	20	3impia	$$⊢\left(K\in V\wedge W\in H\wedge S\in E\right)\to \left(\left(F\in T\wedge G\in T\right)\to S\left(F\circ G\right)=S\left(F\right)\circ S\left(G\right)\right)$$
22	21	imp	$$⊢\left(\left(K\in V\wedge W\in H\wedge S\in E\right)\wedge \left(F\in T\wedge G\in T\right)\right)\to S\left(F\circ G\right)=S\left(F\right)\circ S\left(G\right)$$