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 𝐼 = ( 𝑢𝐸 ↦ ( 𝑔𝑇 ( 𝑢𝑔 ) ) )