**Description:** Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013)

Ref | Expression | ||
---|---|---|---|

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

tendo02.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | ||

Assertion | tendo02 | ⊢ ( 𝐹 ∈ 𝑇 → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) ) |

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

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

2 | tendo02.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |

3 | eqidd | ⊢ ( 𝑔 = 𝐹 → ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) ) | |

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

5 | funi | ⊢ Fun I | |

6 | 2 | fvexi | ⊢ 𝐵 ∈ V |

7 | resfunexg | ⊢ ( ( Fun I ∧ 𝐵 ∈ V ) → ( I ↾ 𝐵 ) ∈ V ) | |

8 | 5 6 7 | mp2an | ⊢ ( I ↾ 𝐵 ) ∈ V |

9 | 3 4 8 | fvmpt | ⊢ ( 𝐹 ∈ 𝑇 → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) ) |