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

Proof

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