Metamath Proof Explorer

Theorem sumeq1

Description: Equality theorem for a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

		Ref	Expression
	Assertion	sumeq1	$⊢ A = B \to \sum_{k \in A} C = \sum_{k \in B} C$

Proof

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