# Metamath Proof Explorer

## Theorem etransclem6

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

Ref Expression
Assertion etransclem6 ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦𝑘 ) ↑ 𝑃 ) ) )

### Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 ↑ ( 𝑃 − 1 ) ) = ( 𝑦 ↑ ( 𝑃 − 1 ) ) )
2 oveq2 ( 𝑗 = 𝑘 → ( 𝑥𝑗 ) = ( 𝑥𝑘 ) )
3 2 oveq1d ( 𝑗 = 𝑘 → ( ( 𝑥𝑗 ) ↑ 𝑃 ) = ( ( 𝑥𝑘 ) ↑ 𝑃 ) )
4 3 cbvprodv 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑘 ) ↑ 𝑃 )
5 oveq1 ( 𝑥 = 𝑦 → ( 𝑥𝑘 ) = ( 𝑦𝑘 ) )
6 5 oveq1d ( 𝑥 = 𝑦 → ( ( 𝑥𝑘 ) ↑ 𝑃 ) = ( ( 𝑦𝑘 ) ↑ 𝑃 ) )
7 6 prodeq2ad ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑘 ) ↑ 𝑃 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦𝑘 ) ↑ 𝑃 ) )
8 4 7 syl5eq ( 𝑥 = 𝑦 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦𝑘 ) ↑ 𝑃 ) )
9 1 8 oveq12d ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) = ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦𝑘 ) ↑ 𝑃 ) ) )
10 9 cbvmptv ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦𝑘 ) ↑ 𝑃 ) ) )