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 {\mathbb{N}}_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 {\mathbb{N}}_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\leftrightarrow \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\leftrightarrow \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 {\mathbb{N}}_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 {\mathbb{N}}_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)$$