Theorem etransclem5

Description: A change of bound variable, often used in proofs for etransc . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Assertion	etransclem5	$$⊢\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)\right)=\left(k\in \left(0\dots M\right)⟼\left(y\in X⟼{\left(y-k\right)}^{if\left(k=0,P-1,P\right)}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=y\to x-j=y-j$$
2	1	oveq1d	$$⊢x=y\to {\left(x-j\right)}^{if\left(j=0,P-1,P\right)}={\left(y-j\right)}^{if\left(j=0,P-1,P\right)}$$
3	2	cbvmptv	$$⊢\left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)=\left(y\in X⟼{\left(y-j\right)}^{if\left(j=0,P-1,P\right)}\right)$$
4		oveq2	$$⊢j=k\to y-j=y-k$$
5		eqeq1	$$⊢j=k\to \left(j=0\leftrightarrow k=0\right)$$
6	5	ifbid	$$⊢j=k\to if\left(j=0,P-1,P\right)=if\left(k=0,P-1,P\right)$$
7	4 6	oveq12d	$$⊢j=k\to {\left(y-j\right)}^{if\left(j=0,P-1,P\right)}={\left(y-k\right)}^{if\left(k=0,P-1,P\right)}$$
8	7	mpteq2dv	$$⊢j=k\to \left(y\in X⟼{\left(y-j\right)}^{if\left(j=0,P-1,P\right)}\right)=\left(y\in X⟼{\left(y-k\right)}^{if\left(k=0,P-1,P\right)}\right)$$
9	3 8	eqtrid	$$⊢j=k\to \left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)=\left(y\in X⟼{\left(y-k\right)}^{if\left(k=0,P-1,P\right)}\right)$$
10	9	cbvmptv	$$⊢\left(j\in \left(0\dots M\right)⟼\left(x\in X⟼{\left(x-j\right)}^{if\left(j=0,P-1,P\right)}\right)\right)=\left(k\in \left(0\dots M\right)⟼\left(y\in X⟼{\left(y-k\right)}^{if\left(k=0,P-1,P\right)}\right)\right)$$