This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tendoicbv

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

		Ref	Expression
	Hypothesis	tendoi.i	⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑠 ‘ 𝑓 ) ) )
	Assertion	tendoicbv	⊢ 𝐼 = ( 𝑢 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ^◡ ( 𝑢 ‘ 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendoi.i	⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑠 ‘ 𝑓 ) ) )
2		fveq1	⊢ ( 𝑠 = 𝑢 → ( 𝑠 ‘ 𝑓 ) = ( 𝑢 ‘ 𝑓 ) )
3	2	cnveqd	⊢ ( 𝑠 = 𝑢 → ^◡ ( 𝑠 ‘ 𝑓 ) = ^◡ ( 𝑢 ‘ 𝑓 ) )
4	3	mpteq2dv	⊢ ( 𝑠 = 𝑢 → ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑠 ‘ 𝑓 ) ) = ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑢 ‘ 𝑓 ) ) )
5		fveq2	⊢ ( 𝑓 = 𝑔 → ( 𝑢 ‘ 𝑓 ) = ( 𝑢 ‘ 𝑔 ) )
6	5	cnveqd	⊢ ( 𝑓 = 𝑔 → ^◡ ( 𝑢 ‘ 𝑓 ) = ^◡ ( 𝑢 ‘ 𝑔 ) )
7	6	cbvmptv	⊢ ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑢 ‘ 𝑓 ) ) = ( 𝑔 ∈ 𝑇 ↦ ^◡ ( 𝑢 ‘ 𝑔 ) )
8	4 7	eqtrdi	⊢ ( 𝑠 = 𝑢 → ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑠 ‘ 𝑓 ) ) = ( 𝑔 ∈ 𝑇 ↦ ^◡ ( 𝑢 ‘ 𝑔 ) ) )
9	8	cbvmptv	⊢ ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑠 ‘ 𝑓 ) ) ) = ( 𝑢 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ^◡ ( 𝑢 ‘ 𝑔 ) ) )
10	1 9	eqtri	⊢ 𝐼 = ( 𝑢 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ^◡ ( 𝑢 ‘ 𝑔 ) ) )