# Metamath Proof Explorer

## Theorem etransclem12

Description: C applied to N . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem12.1 ${⊢}{C}=\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)$
etransclem12.2 ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
Assertion etransclem12 ${⊢}{\phi }\to {C}\left({N}\right)=\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\}$

### Proof

Step Hyp Ref Expression
1 etransclem12.1 ${⊢}{C}=\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)$
2 etransclem12.2 ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
3 oveq2 ${⊢}{n}={N}\to \left(0\dots {n}\right)=\left(0\dots {N}\right)$
4 3 oveq1d ${⊢}{n}={N}\to {\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}={\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}$
5 eqeq2 ${⊢}{n}={N}\to \left(\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}↔\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right)$
6 4 5 rabeqbidv ${⊢}{n}={N}\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 {N}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={N}\right\}$
7 ovex ${⊢}{\left(0\dots {N}\right)}^{\left(0\dots {M}\right)}\in \mathrm{V}$
8 7 rabex ${⊢}\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\}\in \mathrm{V}$
9 8 a1i ${⊢}{\phi }\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\}\in \mathrm{V}$
10 1 6 2 9 fvmptd3 ${⊢}{\phi }\to {C}\left({N}\right)=\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\}$