Metamath Proof Explorer


Theorem tendoi

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

Ref Expression
Hypotheses tendoi.i I = s E f T s f -1
tendoi.t T = LTrn K W
Assertion tendoi S E I S = g T S g -1

Proof

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