cbvsumdavw2

Description: Change bound variable and the set of integers in a sum. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvsumdavw2.1	$⊢ φ \to A = B$
	cbvsumdavw2.2	$⊢ (φ \land j = k) \to C = D$
Assertion	cbvsumdavw2	$⊢ φ \to \sum_{j \in A} C = \sum_{k \in B} D$

Proof

Step	Hyp	Ref	Expression
1		cbvsumdavw2.1	$⊢ φ \to A = B$
2		cbvsumdavw2.2	$⊢ (φ \land j = k) \to C = D$
3	1	sseq1d	$⊢ φ \to (A \subseteq ℤ_{\geq m} \leftrightarrow B \subseteq ℤ_{\geq m})$
4	1	eleq2d	$⊢ φ \to (n \in A \leftrightarrow n \in B)$
5	2	cbvcsbdavw	$⊢ φ \to ⦋ n / j ⦌ C = ⦋ n / k ⦌ D$
6	4 5	ifbieq1d	$⊢ φ \to if (n \in A, ⦋ n / j ⦌ C, 0) = if (n \in B, ⦋ n / k ⦌ D, 0)$
7	6	mpteq2dv	$⊢ φ \to (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ C, 0)) = (n \in ℤ ⟼ if (n \in B, ⦋ n / k ⦌ D, 0))$
8	7	seqeq3d	$⊢ φ \to seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ C, 0))) = seq m (+ (n \in ℤ ⟼ if (n \in B, ⦋ n / k ⦌ D, 0)))$
9	8	breq1d	$⊢ φ \to (seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ C, 0))) ⇝ x \leftrightarrow seq m (+ (n \in ℤ ⟼ if (n \in B, ⦋ n / k ⦌ D, 0))) ⇝ x)$
10	3 9	anbi12d	$⊢ φ \to ((A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ C, 0))) ⇝ x) \leftrightarrow (B \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in B, ⦋ n / k ⦌ D, 0))) ⇝ x))$
11	10	rexbidv	$⊢ φ \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ C, 0))) ⇝ x) \leftrightarrow \exists m \in ℤ (B \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in B, ⦋ n / k ⦌ D, 0))) ⇝ x))$
12	1	f1oeq3d	$⊢ φ \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots m) \underset{1-1 onto}{⟶} B)$
13	2	cbvcsbdavw	$⊢ φ \to ⦋ f (n) / j ⦌ C = ⦋ f (n) / k ⦌ D$
14	13	mpteq2dv	$⊢ φ \to (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)$
15	14	seqeq3d	$⊢ φ \to seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D))$
16	15	fveq1d	$⊢ φ \to seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)$
17	16	eqeq2d	$⊢ φ \to (x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m) \leftrightarrow x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m))$
18	12 17	anbi12d	$⊢ φ \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)))$
19	18	exbidv	$⊢ φ \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)))$
20	19	rexbidv	$⊢ φ \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)))$
21	11 20	orbi12d	$⊢ φ \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ 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) / j ⦌ C)) (m))) \leftrightarrow (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in B, ⦋ n / k ⦌ D, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m))))$
22	21	iotabidv	$⊢ φ \to (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ 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) / j ⦌ C)) (m)))) = (ι x \| (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in B, ⦋ n / k ⦌ D, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m))))$
23		df-sum	$⊢ \sum_{j \in A} C = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / j ⦌ 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) / j ⦌ C)) (m))))$
24		df-sum	$⊢ \sum_{k \in B} D = (ι x \| (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in B, ⦋ n / k ⦌ D, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m))))$
25	22 23 24	3eqtr4g	$⊢ φ \to \sum_{j \in A} C = \sum_{k \in B} D$

Metamath Proof Explorer

Theorem cbvsumdavw2

Proof