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

Metamath Proof Explorer

Theorem tendo0cbv

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

		Ref	Expression
	Hypothesis	tendo0cbv.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
	Assertion	tendo0cbv	$⊢ O = (g \in T ⟼ {I ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		tendo0cbv.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
2		eqidd	$⊢ f = g \to {I ↾}_{B} = {I ↾}_{B}$
3	2	cbvmptv	$⊢ (f \in T ⟼ {I ↾}_{B}) = (g \in T ⟼ {I ↾}_{B})$
4	1 3	eqtri	$⊢ O = (g \in T ⟼ {I ↾}_{B})$