Theorem tendof

Description: Functionality of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013)

	Ref	Expression
Hypotheses	tendof.h	|- H = ( LHyp ` K )
	tendof.t	|- T = ( ( LTrn ` K ) ` W )
	tendof.e	|- E = ( ( TEndo ` K ) ` W )
Assertion	tendof	|- ( ( ( K e. V /\ W e. H ) /\ S e. E ) -> S : T --> T )

Proof

Step	Hyp	Ref	Expression
1		tendof.h	|- H = ( LHyp ` K )
2		tendof.t	|- T = ( ( LTrn ` K ) ` W )
3		tendof.e	|- E = ( ( TEndo ` K ) ` W )
4		eqid	|- ( le ` K ) = ( le ` K )
5		eqid	|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
6	4 1 2 5 3	istendo	|- ( ( K e. V /\ W e. H ) -> ( S e. E <-> ( S : T --> T /\ A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) /\ A. f e. T ( ( ( trL ` K ) ` W ) ` ( S ` f ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` f ) ) ) )
7		simp1	|- ( ( S : T --> T /\ A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) /\ A. f e. T ( ( ( trL ` K ) ` W ) ` ( S ` f ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` f ) ) -> S : T --> T )
8	6 7	syl6bi	|- ( ( K e. V /\ W e. H ) -> ( S e. E -> S : T --> T ) )
9	8	imp	|- ( ( ( K e. V /\ W e. H ) /\ S e. E ) -> S : T --> T )