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 ⊢ j ∈ 0 … M ⟼ x ∈ X ⟼ x − j if j = 0 P − 1 P = k ∈ 0 … M ⟼ y ∈ X ⟼ y − k if k = 0 P − 1 P

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ x = y → x − j = y − j
2 1 oveq1d ⊢ x = y → x − j if j = 0 P − 1 P = y − j if j = 0 P − 1 P
3 2 cbvmptv ⊢ x ∈ X ⟼ x − j if j = 0 P − 1 P = y ∈ X ⟼ y − j if j = 0 P − 1 P
4 oveq2 ⊢ j = k → y − j = y − k
5 eqeq1 ⊢ j = k → j = 0 ↔ k = 0
6 5 ifbid ⊢ j = k → if j = 0 P − 1 P = if k = 0 P − 1 P
7 4 6 oveq12d ⊢ j = k → y − j if j = 0 P − 1 P = y − k if k = 0 P − 1 P
8 7 mpteq2dv ⊢ j = k → y ∈ X ⟼ y − j if j = 0 P − 1 P = y ∈ X ⟼ y − k if k = 0 P − 1 P
9 3 8 syl5eq ⊢ j = k → x ∈ X ⟼ x − j if j = 0 P − 1 P = y ∈ X ⟼ y − k if k = 0 P − 1 P
10 9 cbvmptv ⊢ j ∈ 0 … M ⟼ x ∈ X ⟼ x − j if j = 0 P − 1 P = k ∈ 0 … M ⟼ y ∈ X ⟼ y − k if k = 0 P − 1 P