Metamath Proof Explorer


Theorem tendo0cbv

Description: Define additive identity for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypothesis tendo0cbv.o O=fTIB
Assertion tendo0cbv O=gTIB

Proof

Step Hyp Ref Expression
1 tendo0cbv.o O=fTIB
2 eqidd f=gIB=IB
3 2 cbvmptv fTIB=gTIB
4 1 3 eqtri O=gTIB