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 ⊢ I = s ∈ E ⟼ f ∈ T ⟼ s ⁡ f -1
Assertion tendoicbv ⊢ I = u ∈ E ⟼ g ∈ T ⟼ u ⁡ g -1

Proof

Step Hyp Ref Expression
1 tendoi.i ⊢ I = s ∈ E ⟼ f ∈ T ⟼ s ⁡ f -1
2 fveq1 ⊢ s = u → s ⁡ f = u ⁡ f
3 2 cnveqd ⊢ s = u → s ⁡ f -1 = u ⁡ f -1
4 3 mpteq2dv ⊢ s = u → f ∈ T ⟼ s ⁡ f -1 = f ∈ T ⟼ u ⁡ f -1
5 fveq2 ⊢ f = g → u ⁡ f = u ⁡ g
6 5 cnveqd ⊢ f = g → u ⁡ f -1 = u ⁡ g -1
7 6 cbvmptv ⊢ f ∈ T ⟼ u ⁡ f -1 = g ∈ T ⟼ u ⁡ g -1
8 4 7 eqtrdi ⊢ s = u → f ∈ T ⟼ s ⁡ f -1 = g ∈ T ⟼ u ⁡ g -1
9 8 cbvmptv ⊢ s ∈ E ⟼ f ∈ T ⟼ s ⁡ f -1 = u ∈ E ⟼ g ∈ T ⟼ u ⁡ g -1
10 1 9 eqtri ⊢ I = u ∈ E ⟼ g ∈ T ⟼ u ⁡ g -1