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 ${⊢}\left({n}\in {ℕ}_{0}⟼\left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}\right)=\left({m}\in {ℕ}_{0}⟼\left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={m}\right\}\right)$

Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{n}={m}\to \left(0\dots {n}\right)=\left(0\dots {m}\right)$
2 1 oveq1d ${⊢}{n}={m}\to {\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}={\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}$
3 2 rabeqdv ${⊢}{n}={m}\to \left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}=\left\{{c}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}$
4 fveq2 ${⊢}{j}={k}\to {c}\left({j}\right)={c}\left({k}\right)$
5 4 cbvsumv ${⊢}\sum _{{j}=0}^{{M}}{c}\left({j}\right)=\sum _{{k}=0}^{{M}}{c}\left({k}\right)$
6 fveq1 ${⊢}{c}={d}\to {c}\left({k}\right)={d}\left({k}\right)$
7 6 sumeq2sdv ${⊢}{c}={d}\to \sum _{{k}=0}^{{M}}{c}\left({k}\right)=\sum _{{k}=0}^{{M}}{d}\left({k}\right)$
8 5 7 syl5eq ${⊢}{c}={d}\to \sum _{{j}=0}^{{M}}{c}\left({j}\right)=\sum _{{k}=0}^{{M}}{d}\left({k}\right)$
9 8 eqeq1d ${⊢}{c}={d}\to \left(\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}↔\sum _{{k}=0}^{{M}}{d}\left({k}\right)={n}\right)$
10 9 cbvrabv ${⊢}\left\{{c}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}=\left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={n}\right\}$
11 eqeq2 ${⊢}{n}={m}\to \left(\sum _{{k}=0}^{{M}}{d}\left({k}\right)={n}↔\sum _{{k}=0}^{{M}}{d}\left({k}\right)={m}\right)$
12 11 rabbidv ${⊢}{n}={m}\to \left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={n}\right\}=\left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={m}\right\}$
13 10 12 syl5eq ${⊢}{n}={m}\to \left\{{c}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}=\left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={m}\right\}$
14 3 13 eqtrd ${⊢}{n}={m}\to \left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}=\left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={m}\right\}$
15 14 cbvmptv ${⊢}\left({n}\in {ℕ}_{0}⟼\left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}\right)=\left({m}\in {ℕ}_{0}⟼\left\{{d}\in \left({\left(0\dots {m}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{k}=0}^{{M}}{d}\left({k}\right)={m}\right\}\right)$