# Metamath Proof Explorer

## Theorem etransclem11

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

Ref Expression
Assertion etransclem11 ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } ) = ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑚 } )

### Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑛 = 𝑚 → ( 0 ... 𝑛 ) = ( 0 ... 𝑚 ) )
2 1 oveq1d ( 𝑛 = 𝑚 → ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) = ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) )
3 2 rabeqdv ( 𝑛 = 𝑚 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
4 fveq2 ( 𝑗 = 𝑘 → ( 𝑐𝑗 ) = ( 𝑐𝑘 ) )
5 4 cbvsumv Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑘 )
6 fveq1 ( 𝑐 = 𝑑 → ( 𝑐𝑘 ) = ( 𝑑𝑘 ) )
7 6 sumeq2sdv ( 𝑐 = 𝑑 → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) )
8 5 7 syl5eq ( 𝑐 = 𝑑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) )
9 8 eqeq1d ( 𝑐 = 𝑑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 ↔ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑛 ) )
10 9 cbvrabv { 𝑐 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } = { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑛 }
11 eqeq2 ( 𝑛 = 𝑚 → ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑛 ↔ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑚 ) )
12 11 rabbidv ( 𝑛 = 𝑚 → { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑛 } = { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑚 } )
13 10 12 syl5eq ( 𝑛 = 𝑚 → { 𝑐 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } = { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑚 } )
14 3 13 eqtrd ( 𝑛 = 𝑚 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } = { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑚 } )
15 14 cbvmptv ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } ) = ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑘 ) = 𝑚 } )