**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 | ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) | |

Assertion | tendo0cbv | ⊢ 𝑂 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | tendo0cbv.o | ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) | |

2 | eqidd | ⊢ ( 𝑓 = 𝑔 → ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) ) | |

3 | 2 | cbvmptv | ⊢ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) |

4 | 1 3 | eqtri | ⊢ 𝑂 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) |