Theorem tendocl

Description: Closure 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	tendocl	|- ( ( ( K e. V /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` F ) e. 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	1 2 3	tendof	|- ( ( ( K e. V /\ W e. H ) /\ S e. E ) -> S : T --> T )
5	4	3adant3	|- ( ( ( K e. V /\ W e. H ) /\ S e. E /\ F e. T ) -> S : T --> T )
6		simp3	|- ( ( ( K e. V /\ W e. H ) /\ S e. E /\ F e. T ) -> F e. T )
7	5 6	ffvelcdmd	|- ( ( ( K e. V /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` F ) e. T )