Theorem tendoi

Description: Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013)

	Ref	Expression
Hypotheses	tendoi.i	|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )
	tendoi.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	tendoi	|- ( S e. E -> ( I ` S ) = ( g e. T |-> `' ( S ` g ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendoi.i	|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )
2		tendoi.t	|- T = ( ( LTrn ` K ) ` W )
3		fveq1	|- ( u = S -> ( u ` g ) = ( S ` g ) )
4	3	cnveqd	|- ( u = S -> `' ( u ` g ) = `' ( S ` g ) )
5	4	mpteq2dv	|- ( u = S -> ( g e. T |-> `' ( u ` g ) ) = ( g e. T |-> `' ( S ` g ) ) )
6	1	tendoicbv	|- I = ( u e. E |-> ( g e. T |-> `' ( u ` g ) ) )
7	5 6 2	mptfvmpt	|- ( S e. E -> ( I ` S ) = ( g e. T |-> `' ( S ` g ) ) )