Theorem tendo02

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

	Ref	Expression
Hypotheses	tendo0cbv.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	tendo02.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
Assertion	tendo02	⊢ ( 𝐹 ∈ 𝑇 → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) )

Proof

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 ↾ 𝐵 ) )