Metamath Proof Explorer


Theorem tendoi2

Description: Value of additive 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 tendoi2 S E F T I S F = S F -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 1 2 tendoi S E I S = g T S g -1
4 3 adantr S E F T I S = g T S g -1
5 fveq2 g = F S g = S F
6 5 cnveqd g = F S g -1 = S F -1
7 6 adantl S E F T g = F S g -1 = S F -1
8 simpr S E F T F T
9 fvex S F V
10 9 cnvex S F -1 V
11 10 a1i S E F T S F -1 V
12 4 7 8 11 fvmptd S E F T I S F = S F -1