sumeq2sdv

Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006) (Proof shortened by Glauco Siliprandi, 5-Apr-2020) Avoid axioms. (Revised by GG, 14-Aug-2025)

		Ref	Expression
	Hypothesis	sumeq2sdv.1	$⊢ φ \to B = C$
	Assertion	sumeq2sdv	$⊢ φ \to \sum_{k \in A} B = \sum_{k \in A} C$

Proof

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

Metamath Proof Explorer

Theorem sumeq2sdv

Proof