# Metamath Proof Explorer

## 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↔{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 syl5eq ${⊢}{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)$