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

Metamath Proof Explorer

Theorem tendoplcbv

Description: Define sum operation for trace-preserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypothesis tendoplcbv.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
Assertion tendoplcbv ⊢ P = u ∈ E , v ∈ E ⟼ g ∈ T ⟼ u ⁡ g ∘ v ⁡ g

Proof

Step Hyp Ref Expression
1 tendoplcbv.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
2 fveq1 ⊢ s = u → s ⁡ f = u ⁡ f
3 2 coeq1d ⊢ s = u → s ⁡ f ∘ t ⁡ f = u ⁡ f ∘ t ⁡ f
4 3 mpteq2dv ⊢ s = u → f ∈ T ⟼ s ⁡ f ∘ t ⁡ f = f ∈ T ⟼ u ⁡ f ∘ t ⁡ f
5 fveq1 ⊢ t = v → t ⁡ f = v ⁡ f
6 5 coeq2d ⊢ t = v → u ⁡ f ∘ t ⁡ f = u ⁡ f ∘ v ⁡ f
7 6 mpteq2dv ⊢ t = v → f ∈ T ⟼ u ⁡ f ∘ t ⁡ f = f ∈ T ⟼ u ⁡ f ∘ v ⁡ f
8 fveq2 ⊢ f = g → u ⁡ f = u ⁡ g
9 fveq2 ⊢ f = g → v ⁡ f = v ⁡ g
10 8 9 coeq12d ⊢ f = g → u ⁡ f ∘ v ⁡ f = u ⁡ g ∘ v ⁡ g
11 10 cbvmptv ⊢ f ∈ T ⟼ u ⁡ f ∘ v ⁡ f = g ∈ T ⟼ u ⁡ g ∘ v ⁡ g
12 7 11 eqtrdi ⊢ t = v → f ∈ T ⟼ u ⁡ f ∘ t ⁡ f = g ∈ T ⟼ u ⁡ g ∘ v ⁡ g
13 4 12 cbvmpov ⊢ s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f = u ∈ E , v ∈ E ⟼ g ∈ T ⟼ u ⁡ g ∘ v ⁡ g
14 1 13 eqtri ⊢ P = u ∈ E , v ∈ E ⟼ g ∈ T ⟼ u ⁡ g ∘ v ⁡ g