cbvsumv

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)

		Ref	Expression
	Hypothesis	cbvsum.1	$⊢ j = k \to B = C$
	Assertion	cbvsumv	$⊢ \sum_{j \in A} B = \sum_{k \in A} C$

Proof

Step	Hyp	Ref	Expression
1		cbvsum.1	$⊢ j = k \to B = C$
2	1	cbvcsbv	$⊢ ⦋ n / j ⦌ B = ⦋ n / k ⦌ C$
3	2	a1i	$⊢ ⊤ \to ⦋ n / j ⦌ B = ⦋ n / k ⦌ C$
4	3	ifeq1d	$⊢ ⊤ \to if (n \in A, ⦋ n / j ⦌ B, 0) = if (n \in A, ⦋ n / k ⦌ C, 0)$
5	4	mpteq2dv	$⊢ ⊤ \to (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0)) = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))$
6	5	seqeq3d	$⊢ ⊤ \to seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0))) = seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0)))$
7	6	breq1d	$⊢ ⊤ \to (seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0))) ⇝ x \leftrightarrow seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))) ⇝ x)$
8	7	mptru	$⊢ seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0))) ⇝ x \leftrightarrow seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))) ⇝ x$
9	8	anbi2i	$⊢ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0))) ⇝ x) \leftrightarrow (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))) ⇝ x)$
10	9	rexbii	$⊢ \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0))) ⇝ x) \leftrightarrow \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))) ⇝ x)$
11	1	cbvcsbv	$⊢ ⦋ f (n) / j ⦌ B = ⦋ f (n) / k ⦌ C$
12	11	mpteq2i	$⊢ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)$
13	12	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)$
14	13	seqeq3d	$⊢ ⊤ \to seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C))$
15	14	mptru	$⊢ seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C))$
16	15	fveq1i	$⊢ seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)$
17	16	eqeq2i	$⊢ x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m) \leftrightarrow x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)$
18	17	anbi2i	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
19	18	exbii	$⊢ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
20	19	rexbii	$⊢ \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
21	10 20	orbi12i	$⊢ (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m))) \leftrightarrow (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)))$
22	21	iotabii	$⊢ (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m)))) = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))))$
23		df-sum	$⊢ \sum_{j \in A} B = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m))))$
24		df-sum	$⊢ \sum_{k \in A} C = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))))$
25	22 23 24	3eqtr4i	$⊢ \sum_{j \in A} B = \sum_{k \in A} C$

Metamath Proof Explorer

Theorem cbvsumv

Proof