Theorem tendo1mul

Description: Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-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	tendo1mul	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge U\in E\right)\to \left({\mathrm{I}\upharpoonright }_T\right)\circ U=U$$

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	1 2 3	tendof	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge U\in E\right)\to U:T⟶T$$
5		fcoi2	$$⊢U:T⟶T\to \left({\mathrm{I}\upharpoonright }_T\right)\circ U=U$$
6	4 5	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge U\in E\right)\to \left({\mathrm{I}\upharpoonright }_T\right)\circ U=U$$