sumeq2ii

Description: Equality theorem for sum, with the class expressions B and C guarded by _I to be always sets. (Contributed by Mario Carneiro, 13-Jun-2019)

		Ref	Expression
	Assertion	sumeq2ii	$⊢ \forall k \in A I (B) = I (C) \to \sum_{k \in A} B = \sum_{k \in A} C$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \to m \in ℤ$
2		simpr	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \land n \in A) \to n \in A$
3		simplll	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \land n \in A) \to \forall k \in A I (B) = I (C)$
4		nfcv	$⊢ \underline{Ⅎ} k I$
5		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ B$
6	4 5	nffv	$⊢ \underline{Ⅎ} k I (⦋ n / k ⦌ B)$
7		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ C$
8	4 7	nffv	$⊢ \underline{Ⅎ} k I (⦋ n / k ⦌ C)$
9	6 8	nfeq	$⊢ Ⅎ k I (⦋ n / k ⦌ B) = I (⦋ n / k ⦌ C)$
10		csbeq1a	$⊢ k = n \to B = ⦋ n / k ⦌ B$
11	10	fveq2d	$⊢ k = n \to I (B) = I (⦋ n / k ⦌ B)$
12		csbeq1a	$⊢ k = n \to C = ⦋ n / k ⦌ C$
13	12	fveq2d	$⊢ k = n \to I (C) = I (⦋ n / k ⦌ C)$
14	11 13	eqeq12d	$⊢ k = n \to (I (B) = I (C) \leftrightarrow I (⦋ n / k ⦌ B) = I (⦋ n / k ⦌ C))$
15	9 14	rspc	$⊢ n \in A \to (\forall k \in A I (B) = I (C) \to I (⦋ n / k ⦌ B) = I (⦋ n / k ⦌ C))$
16	2 3 15	sylc	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \land n \in A) \to I (⦋ n / k ⦌ B) = I (⦋ n / k ⦌ C)$
17	16	ifeq1da	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \to if (n \in A, I (⦋ n / k ⦌ B), I (0)) = if (n \in A, I (⦋ n / k ⦌ C), I (0))$
18		fvif	$⊢ I (if (n \in A, ⦋ n / k ⦌ B, 0)) = if (n \in A, I (⦋ n / k ⦌ B), I (0))$
19		fvif	$⊢ I (if (n \in A, ⦋ n / k ⦌ C, 0)) = if (n \in A, I (⦋ n / k ⦌ C), I (0))$
20	17 18 19	3eqtr4g	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \to I (if (n \in A, ⦋ n / k ⦌ B, 0)) = I (if (n \in A, ⦋ n / k ⦌ C, 0))$
21	20	mpteq2dv	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \to (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ B, 0))) = (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ C, 0)))$
22	21	fveq1d	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \to (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ B, 0))) (x) = (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ C, 0))) (x)$
23		eqid	$⊢ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))$
24		eqid	$⊢ (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ B, 0))) = (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ B, 0)))$
25	23 24	fvmptex	$⊢ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) (x) = (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ B, 0))) (x)$
26		eqid	$⊢ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0)) = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0))$
27		eqid	$⊢ (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ C, 0))) = (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ C, 0)))$
28	26 27	fvmptex	$⊢ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0)) (x) = (n \in ℤ ⟼ I (if (n \in A, ⦋ n / k ⦌ C, 0))) (x)$
29	22 25 28	3eqtr4g	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \to (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) (x) = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ C, 0)) (x)$
30	1 29	seqfeq	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \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)))$
31	30	breq1d	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \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)$
32	31	anbi2d	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \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))$
33	32	rexbidva	$⊢ \forall k \in A I (B) = I (C) \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))$
34		simplr	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to m \in ℕ$
35		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
36	34 35	eleqtrdi	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to m \in ℤ_{\geq 1}$
37		f1of	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} A \to f : (1 \dots m) ⟶ A$
38	37	ad2antlr	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to f : (1 \dots m) ⟶ A$
39		ffvelrn	$⊢ (f : (1 \dots m) ⟶ A \land x \in (1 \dots m)) \to f (x) \in A$
40	38 39	sylancom	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to f (x) \in A$
41		simplll	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to \forall k \in A I (B) = I (C)$
42		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ f (x) / k ⦌ I (B)$
43		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ f (x) / k ⦌ I (C)$
44	42 43	nfeq	$⊢ Ⅎ k ⦋ f (x) / k ⦌ I (B) = ⦋ f (x) / k ⦌ I (C)$
45		csbeq1a	$⊢ k = f (x) \to I (B) = ⦋ f (x) / k ⦌ I (B)$
46		csbeq1a	$⊢ k = f (x) \to I (C) = ⦋ f (x) / k ⦌ I (C)$
47	45 46	eqeq12d	$⊢ k = f (x) \to (I (B) = I (C) \leftrightarrow ⦋ f (x) / k ⦌ I (B) = ⦋ f (x) / k ⦌ I (C))$
48	44 47	rspc	$⊢ f (x) \in A \to (\forall k \in A I (B) = I (C) \to ⦋ f (x) / k ⦌ I (B) = ⦋ f (x) / k ⦌ I (C))$
49	40 41 48	sylc	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to ⦋ f (x) / k ⦌ I (B) = ⦋ f (x) / k ⦌ I (C)$
50		fvex	$⊢ f (x) \in V$
51		csbfv2g	$⊢ f (x) \in V \to ⦋ f (x) / k ⦌ I (B) = I (⦋ f (x) / k ⦌ B)$
52	50 51	ax-mp	$⊢ ⦋ f (x) / k ⦌ I (B) = I (⦋ f (x) / k ⦌ B)$
53		csbfv2g	$⊢ f (x) \in V \to ⦋ f (x) / k ⦌ I (C) = I (⦋ f (x) / k ⦌ C)$
54	50 53	ax-mp	$⊢ ⦋ f (x) / k ⦌ I (C) = I (⦋ f (x) / k ⦌ C)$
55	49 52 54	3eqtr3g	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to I (⦋ f (x) / k ⦌ B) = I (⦋ f (x) / k ⦌ C)$
56		elfznn	$⊢ x \in (1 \dots m) \to x \in ℕ$
57	56	adantl	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to x \in ℕ$
58		fveq2	$⊢ n = x \to f (n) = f (x)$
59	58	csbeq1d	$⊢ n = x \to ⦋ f (n) / k ⦌ B = ⦋ f (x) / k ⦌ B$
60		eqid	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
61	59 60	fvmpti	$⊢ x \in ℕ \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) (x) = I (⦋ f (x) / k ⦌ B)$
62	57 61	syl	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) (x) = I (⦋ f (x) / k ⦌ B)$
63	58	csbeq1d	$⊢ n = x \to ⦋ f (n) / k ⦌ C = ⦋ f (x) / k ⦌ C$
64		eqid	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)$
65	63 64	fvmpti	$⊢ x \in ℕ \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) (x) = I (⦋ f (x) / k ⦌ C)$
66	57 65	syl	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) (x) = I (⦋ f (x) / k ⦌ C)$
67	55 62 66	3eqtr4d	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) (x) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) (x)$
68	36 67	seqfveq	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)$
69	68	eqeq2d	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \leftrightarrow x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
70	69	pm5.32da	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℕ) \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)))$
71	70	exbidv	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℕ) \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)))$
72	71	rexbidva	$⊢ \forall k \in A I (B) = I (C) \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)))$
73	33 72	orbi12d	$⊢ \forall k \in A I (B) = I (C) \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))))$
74	73	iotabidv	$⊢ \forall k \in A I (B) = I (C) \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))))$
75		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))))$
76		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))))$
77	74 75 76	3eqtr4g	$⊢ \forall k \in A I (B) = I (C) \to \sum_{k \in A} B = \sum_{k \in A} C$

Metamath Proof Explorer

Theorem sumeq2ii

Proof