Theorem tendoi

Description: Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013)

	Ref	Expression
Hypotheses	tendoi.i	⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) )
	tendoi.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion	tendoi	⊢ ( 𝑆 ∈ 𝐸 → ( 𝐼 ‘ 𝑆 ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendoi.i	⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) )
2		tendoi.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3		fveq1	⊢ ( 𝑢 = 𝑆 → ( 𝑢 ‘ 𝑔 ) = ( 𝑆 ‘ 𝑔 ) )
4	3	cnveqd	⊢ ( 𝑢 = 𝑆 → ◡ ( 𝑢 ‘ 𝑔 ) = ◡ ( 𝑆 ‘ 𝑔 ) )
5	4	mpteq2dv	⊢ ( 𝑢 = 𝑆 → ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑢 ‘ 𝑔 ) ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) )
6	1	tendoicbv	⊢ 𝐼 = ( 𝑢 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑢 ‘ 𝑔 ) ) )
7	5 6 2	mptfvmpt	⊢ ( 𝑆 ∈ 𝐸 → ( 𝐼 ‘ 𝑆 ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) )