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 ... 𝑛 ) ↑_m ( 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 ... 𝑛 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } ) = ( 𝑚 ∈ ℕ₀ ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } )