dvmptfsum

Description: Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014)

	Ref	Expression
Hypotheses	dvmptfsum.j	$⊢ J = K ↾_{𝑡} S$
	dvmptfsum.k	$⊢ K = TopOpen (ℂ_{fld})$
	dvmptfsum.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvmptfsum.x	$⊢ φ \to X \in J$
	dvmptfsum.i	$⊢ φ \to I \in Fin$
	dvmptfsum.a	$⊢ (φ \land i \in I \land x \in X) \to A \in ℂ$
	dvmptfsum.b	$⊢ (φ \land i \in I \land x \in X) \to B \in ℂ$
	dvmptfsum.d	$⊢ (φ \land i \in I) \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B)$
Assertion	dvmptfsum	$⊢ φ \to \frac{d (x \in X⟼ \sum_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in I} B)$

Proof

Step	Hyp	Ref	Expression
1		dvmptfsum.j	$⊢ J = K ↾_{𝑡} S$
2		dvmptfsum.k	$⊢ K = TopOpen (ℂ_{fld})$
3		dvmptfsum.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
4		dvmptfsum.x	$⊢ φ \to X \in J$
5		dvmptfsum.i	$⊢ φ \to I \in Fin$
6		dvmptfsum.a	$⊢ (φ \land i \in I \land x \in X) \to A \in ℂ$
7		dvmptfsum.b	$⊢ (φ \land i \in I \land x \in X) \to B \in ℂ$
8		dvmptfsum.d	$⊢ (φ \land i \in I) \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B)$
9		ssid	$⊢ I \subseteq I$
10		sseq1	$⊢ a = \emptyset \to (a \subseteq I \leftrightarrow \emptyset \subseteq I)$
11		sumeq1	$⊢ a = \emptyset \to \sum_{i \in a} A = \sum_{i \in \emptyset} A$
12	11	mpteq2dv	$⊢ a = \emptyset \to (x \in X ⟼ \sum_{i \in a} A) = (x \in X ⟼ \sum_{i \in \emptyset} A)$
13	12	oveq2d	$⊢ a = \emptyset \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = \frac{d (x \in X⟼ \sum_{i \in \emptyset} A)}{d_{S} x}$
14		sumeq1	$⊢ a = \emptyset \to \sum_{i \in a} B = \sum_{i \in \emptyset} B$
15	14	mpteq2dv	$⊢ a = \emptyset \to (x \in X ⟼ \sum_{i \in a} B) = (x \in X ⟼ \sum_{i \in \emptyset} B)$
16	13 15	eqeq12d	$⊢ a = \emptyset \to (\frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B) \leftrightarrow \frac{d (x \in X⟼ \sum_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in \emptyset} B))$
17	10 16	imbi12d	$⊢ a = \emptyset \to ((a \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B)) \leftrightarrow (\emptyset \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in \emptyset} B)))$
18	17	imbi2d	$⊢ a = \emptyset \to ((φ \to (a \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B))) \leftrightarrow (φ \to (\emptyset \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in \emptyset} B))))$
19		sseq1	$⊢ a = b \to (a \subseteq I \leftrightarrow b \subseteq I)$
20		sumeq1	$⊢ a = b \to \sum_{i \in a} A = \sum_{i \in b} A$
21	20	mpteq2dv	$⊢ a = b \to (x \in X ⟼ \sum_{i \in a} A) = (x \in X ⟼ \sum_{i \in b} A)$
22	21	oveq2d	$⊢ a = b \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x}$
23		sumeq1	$⊢ a = b \to \sum_{i \in a} B = \sum_{i \in b} B$
24	23	mpteq2dv	$⊢ a = b \to (x \in X ⟼ \sum_{i \in a} B) = (x \in X ⟼ \sum_{i \in b} B)$
25	22 24	eqeq12d	$⊢ a = b \to (\frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B) \leftrightarrow \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))$
26	19 25	imbi12d	$⊢ a = b \to ((a \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B)) \leftrightarrow (b \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B)))$
27	26	imbi2d	$⊢ a = b \to ((φ \to (a \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B))) \leftrightarrow (φ \to (b \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))))$
28		sseq1	$⊢ a = b \cup \{c\} \to (a \subseteq I \leftrightarrow b \cup \{c\} \subseteq I)$
29		sumeq1	$⊢ a = b \cup \{c\} \to \sum_{i \in a} A = \sum_{i \in b \cup \{c\}} A$
30	29	mpteq2dv	$⊢ a = b \cup \{c\} \to (x \in X ⟼ \sum_{i \in a} A) = (x \in X ⟼ \sum_{i \in b \cup \{c\}} A)$
31	30	oveq2d	$⊢ a = b \cup \{c\} \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x}$
32		sumeq1	$⊢ a = b \cup \{c\} \to \sum_{i \in a} B = \sum_{i \in b \cup \{c\}} B$
33	32	mpteq2dv	$⊢ a = b \cup \{c\} \to (x \in X ⟼ \sum_{i \in a} B) = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B)$
34	31 33	eqeq12d	$⊢ a = b \cup \{c\} \to (\frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B) \leftrightarrow \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B))$
35	28 34	imbi12d	$⊢ a = b \cup \{c\} \to ((a \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B)) \leftrightarrow (b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B)))$
36	35	imbi2d	$⊢ a = b \cup \{c\} \to ((φ \to (a \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B))) \leftrightarrow (φ \to (b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B))))$
37		sseq1	$⊢ a = I \to (a \subseteq I \leftrightarrow I \subseteq I)$
38		sumeq1	$⊢ a = I \to \sum_{i \in a} A = \sum_{i \in I} A$
39	38	mpteq2dv	$⊢ a = I \to (x \in X ⟼ \sum_{i \in a} A) = (x \in X ⟼ \sum_{i \in I} A)$
40	39	oveq2d	$⊢ a = I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = \frac{d (x \in X⟼ \sum_{i \in I} A)}{d_{S} x}$
41		sumeq1	$⊢ a = I \to \sum_{i \in a} B = \sum_{i \in I} B$
42	41	mpteq2dv	$⊢ a = I \to (x \in X ⟼ \sum_{i \in a} B) = (x \in X ⟼ \sum_{i \in I} B)$
43	40 42	eqeq12d	$⊢ a = I \to (\frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B) \leftrightarrow \frac{d (x \in X⟼ \sum_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in I} B))$
44	37 43	imbi12d	$⊢ a = I \to ((a \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B)) \leftrightarrow (I \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in I} B)))$
45	44	imbi2d	$⊢ a = I \to ((φ \to (a \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in a} B))) \leftrightarrow (φ \to (I \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in I} B))))$
46		0cnd	$⊢ (φ \land x \in S) \to 0 \in ℂ$
47		0cnd	$⊢ φ \to 0 \in ℂ$
48	3 47	dvmptc	$⊢ φ \to \frac{d (x \in S⟼ 0)}{d_{S} x} = (x \in S ⟼ 0)$
49	2	cnfldtopon	$⊢ K \in TopOn (ℂ)$
50		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
51	3 50	syl	$⊢ φ \to S \subseteq ℂ$
52		resttopon	$⊢ (K \in TopOn (ℂ) \land S \subseteq ℂ) \to K ↾_{𝑡} S \in TopOn (S)$
53	49 51 52	sylancr	$⊢ φ \to K ↾_{𝑡} S \in TopOn (S)$
54	1 53	eqeltrid	$⊢ φ \to J \in TopOn (S)$
55		toponss	$⊢ (J \in TopOn (S) \land X \in J) \to X \subseteq S$
56	54 4 55	syl2anc	$⊢ φ \to X \subseteq S$
57	3 46 46 48 56 1 2 4	dvmptres	$⊢ φ \to \frac{d (x \in X⟼ 0)}{d_{S} x} = (x \in X ⟼ 0)$
58		sum0	$⊢ \sum_{i \in \emptyset} A = 0$
59	58	mpteq2i	$⊢ (x \in X ⟼ \sum_{i \in \emptyset} A) = (x \in X ⟼ 0)$
60	59	oveq2i	$⊢ \frac{d (x \in X⟼ \sum_{i \in \emptyset} A)}{d_{S} x} = \frac{d (x \in X⟼ 0)}{d_{S} x}$
61		sum0	$⊢ \sum_{i \in \emptyset} B = 0$
62	61	mpteq2i	$⊢ (x \in X ⟼ \sum_{i \in \emptyset} B) = (x \in X ⟼ 0)$
63	57 60 62	3eqtr4g	$⊢ φ \to \frac{d (x \in X⟼ \sum_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in \emptyset} B)$
64	63	a1d	$⊢ φ \to (\emptyset \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in \emptyset} B))$
65		ssun1	$⊢ b \subseteq b \cup \{c\}$
66		sstr	$⊢ (b \subseteq b \cup \{c\} \land b \cup \{c\} \subseteq I) \to b \subseteq I$
67	65 66	mpan	$⊢ b \cup \{c\} \subseteq I \to b \subseteq I$
68	67	imim1i	$⊢ (b \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B)) \to (b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))$
69		simpll	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to φ$
70	69 3	syl	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to S \in \{ℝ, ℂ\}$
71	5	ad3antrrr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to I \in Fin$
72	67	ad2antlr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to b \subseteq I$
73	71 72	ssfid	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to b \in Fin$
74		simp-4l	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in b) \to φ$
75	72	sselda	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in b) \to i \in I$
76		simplr	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in b) \to a \in X$
77		nfv	$⊢ Ⅎ x (φ \land i \in I \land a \in X)$
78		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ A$
79	78	nfel1	$⊢ Ⅎ x ⦋ a / x ⦌ A \in ℂ$
80	77 79	nfim	$⊢ Ⅎ x ((φ \land i \in I \land a \in X) \to ⦋ a / x ⦌ A \in ℂ)$
81		eleq1w	$⊢ x = a \to (x \in X \leftrightarrow a \in X)$
82	81	3anbi3d	$⊢ x = a \to ((φ \land i \in I \land x \in X) \leftrightarrow (φ \land i \in I \land a \in X))$
83		csbeq1a	$⊢ x = a \to A = ⦋ a / x ⦌ A$
84	83	eleq1d	$⊢ x = a \to (A \in ℂ \leftrightarrow ⦋ a / x ⦌ A \in ℂ)$
85	82 84	imbi12d	$⊢ x = a \to (((φ \land i \in I \land x \in X) \to A \in ℂ) \leftrightarrow ((φ \land i \in I \land a \in X) \to ⦋ a / x ⦌ A \in ℂ))$
86	80 85 6	chvarfv	$⊢ (φ \land i \in I \land a \in X) \to ⦋ a / x ⦌ A \in ℂ$
87	74 75 76 86	syl3anc	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in b) \to ⦋ a / x ⦌ A \in ℂ$
88	73 87	fsumcl	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in b} ⦋ a / x ⦌ A \in ℂ$
89	88	adantlrr	$⊢ (((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \land a \in X) \to \sum_{i \in b} ⦋ a / x ⦌ A \in ℂ$
90		sumex	$⊢ \sum_{i \in b} ⦋ a / x ⦌ B \in V$
91	90	a1i	$⊢ (((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \land a \in X) \to \sum_{i \in b} ⦋ a / x ⦌ B \in V$
92		nfcv	$⊢ \underline{Ⅎ} a \sum_{i \in b} A$
93		nfcv	$⊢ \underline{Ⅎ} x b$
94	93 78	nfsum	$⊢ \underline{Ⅎ} x \sum_{i \in b} ⦋ a / x ⦌ A$
95	83	sumeq2sdv	$⊢ x = a \to \sum_{i \in b} A = \sum_{i \in b} ⦋ a / x ⦌ A$
96	92 94 95	cbvmpt	$⊢ (x \in X ⟼ \sum_{i \in b} A) = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ A)$
97	96	oveq2i	$⊢ \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = \frac{d (a \in X⟼ \sum_{i \in b} ⦋ a / x ⦌ A)}{d_{S} a}$
98		nfcv	$⊢ \underline{Ⅎ} a \sum_{i \in b} B$
99		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ B$
100	93 99	nfsum	$⊢ \underline{Ⅎ} x \sum_{i \in b} ⦋ a / x ⦌ B$
101		csbeq1a	$⊢ x = a \to B = ⦋ a / x ⦌ B$
102	101	sumeq2sdv	$⊢ x = a \to \sum_{i \in b} B = \sum_{i \in b} ⦋ a / x ⦌ B$
103	98 100 102	cbvmpt	$⊢ (x \in X ⟼ \sum_{i \in b} B) = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ B)$
104	97 103	eqeq12i	$⊢ \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B) \leftrightarrow \frac{d (a \in X⟼ \sum_{i \in b} ⦋ a / x ⦌ A)}{d_{S} a} = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ B)$
105	104	biimpi	$⊢ \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B) \to \frac{d (a \in X⟼ \sum_{i \in b} ⦋ a / x ⦌ A)}{d_{S} a} = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ B)$
106	105	ad2antll	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to \frac{d (a \in X⟼ \sum_{i \in b} ⦋ a / x ⦌ A)}{d_{S} a} = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ B)$
107		simplll	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to φ$
108		ssun2	$⊢ \{c\} \subseteq b \cup \{c\}$
109		sstr	$⊢ (\{c\} \subseteq b \cup \{c\} \land b \cup \{c\} \subseteq I) \to \{c\} \subseteq I$
110	108 109	mpan	$⊢ b \cup \{c\} \subseteq I \to \{c\} \subseteq I$
111		vex	$⊢ c \in V$
112	111	snss	$⊢ c \in I \leftrightarrow \{c\} \subseteq I$
113	110 112	sylibr	$⊢ b \cup \{c\} \subseteq I \to c \in I$
114	113	ad2antlr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to c \in I$
115		simpr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to a \in X$
116	6	3expb	$⊢ (φ \land (i \in I \land x \in X)) \to A \in ℂ$
117	116	ancom2s	$⊢ (φ \land (x \in X \land i \in I)) \to A \in ℂ$
118	117	ralrimivva	$⊢ φ \to \forall x \in X \forall i \in I A \in ℂ$
119		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ c / i ⦌ ⦋ a / x ⦌ A$
120	119	nfel1	$⊢ Ⅎ i ⦋ c / i ⦌ ⦋ a / x ⦌ A \in ℂ$
121		csbeq1a	$⊢ i = c \to ⦋ a / x ⦌ A = ⦋ c / i ⦌ ⦋ a / x ⦌ A$
122	121	eleq1d	$⊢ i = c \to (⦋ a / x ⦌ A \in ℂ \leftrightarrow ⦋ c / i ⦌ ⦋ a / x ⦌ A \in ℂ)$
123	79 120 84 122	rspc2	$⊢ (a \in X \land c \in I) \to (\forall x \in X \forall i \in I A \in ℂ \to ⦋ c / i ⦌ ⦋ a / x ⦌ A \in ℂ)$
124	123	ancoms	$⊢ (c \in I \land a \in X) \to (\forall x \in X \forall i \in I A \in ℂ \to ⦋ c / i ⦌ ⦋ a / x ⦌ A \in ℂ)$
125	118 124	mpan9	$⊢ (φ \land (c \in I \land a \in X)) \to ⦋ c / i ⦌ ⦋ a / x ⦌ A \in ℂ$
126	107 114 115 125	syl12anc	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to ⦋ c / i ⦌ ⦋ a / x ⦌ A \in ℂ$
127	126	adantlrr	$⊢ (((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \land a \in X) \to ⦋ c / i ⦌ ⦋ a / x ⦌ A \in ℂ$
128	7	3expb	$⊢ (φ \land (i \in I \land x \in X)) \to B \in ℂ$
129	128	ancom2s	$⊢ (φ \land (x \in X \land i \in I)) \to B \in ℂ$
130	129	ralrimivva	$⊢ φ \to \forall x \in X \forall i \in I B \in ℂ$
131	99	nfel1	$⊢ Ⅎ x ⦋ a / x ⦌ B \in ℂ$
132		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ c / i ⦌ ⦋ a / x ⦌ B$
133	132	nfel1	$⊢ Ⅎ i ⦋ c / i ⦌ ⦋ a / x ⦌ B \in ℂ$
134	101	eleq1d	$⊢ x = a \to (B \in ℂ \leftrightarrow ⦋ a / x ⦌ B \in ℂ)$
135		csbeq1a	$⊢ i = c \to ⦋ a / x ⦌ B = ⦋ c / i ⦌ ⦋ a / x ⦌ B$
136	135	eleq1d	$⊢ i = c \to (⦋ a / x ⦌ B \in ℂ \leftrightarrow ⦋ c / i ⦌ ⦋ a / x ⦌ B \in ℂ)$
137	131 133 134 136	rspc2	$⊢ (a \in X \land c \in I) \to (\forall x \in X \forall i \in I B \in ℂ \to ⦋ c / i ⦌ ⦋ a / x ⦌ B \in ℂ)$
138	137	ancoms	$⊢ (c \in I \land a \in X) \to (\forall x \in X \forall i \in I B \in ℂ \to ⦋ c / i ⦌ ⦋ a / x ⦌ B \in ℂ)$
139	130 138	mpan9	$⊢ (φ \land (c \in I \land a \in X)) \to ⦋ c / i ⦌ ⦋ a / x ⦌ B \in ℂ$
140	107 114 115 139	syl12anc	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to ⦋ c / i ⦌ ⦋ a / x ⦌ B \in ℂ$
141	140	adantlrr	$⊢ (((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \land a \in X) \to ⦋ c / i ⦌ ⦋ a / x ⦌ B \in ℂ$
142	113	ad2antrl	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to c \in I$
143		nfv	$⊢ Ⅎ i (φ \land c \in I)$
144		nfcv	$⊢ \underline{Ⅎ} i S$
145		nfcv	$⊢ \underline{Ⅎ} i D$
146		nfcv	$⊢ \underline{Ⅎ} i X$
147		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ c / i ⦌ A$
148	146 147	nfmpt	$⊢ \underline{Ⅎ} i (x \in X ⟼ ⦋ c / i ⦌ A)$
149	144 145 148	nfov	$⊢ \underline{Ⅎ} i \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x}$
150		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ c / i ⦌ B$
151	146 150	nfmpt	$⊢ \underline{Ⅎ} i (x \in X ⟼ ⦋ c / i ⦌ B)$
152	149 151	nfeq	$⊢ Ⅎ i \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / i ⦌ B)$
153	143 152	nfim	$⊢ Ⅎ i ((φ \land c \in I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / i ⦌ B))$
154		eleq1w	$⊢ i = c \to (i \in I \leftrightarrow c \in I)$
155	154	anbi2d	$⊢ i = c \to ((φ \land i \in I) \leftrightarrow (φ \land c \in I))$
156		csbeq1a	$⊢ i = c \to A = ⦋ c / i ⦌ A$
157	156	mpteq2dv	$⊢ i = c \to (x \in X ⟼ A) = (x \in X ⟼ ⦋ c / i ⦌ A)$
158	157	oveq2d	$⊢ i = c \to \frac{d (x \in X⟼ A)}{d_{S} x} = \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x}$
159		csbeq1a	$⊢ i = c \to B = ⦋ c / i ⦌ B$
160	159	mpteq2dv	$⊢ i = c \to (x \in X ⟼ B) = (x \in X ⟼ ⦋ c / i ⦌ B)$
161	158 160	eqeq12d	$⊢ i = c \to (\frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B) \leftrightarrow \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / i ⦌ B))$
162	155 161	imbi12d	$⊢ i = c \to (((φ \land i \in I) \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B)) \leftrightarrow ((φ \land c \in I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / i ⦌ B)))$
163	153 162 8	chvarfv	$⊢ (φ \land c \in I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / i ⦌ B)$
164		nfcv	$⊢ \underline{Ⅎ} a ⦋ c / i ⦌ A$
165		nfcv	$⊢ \underline{Ⅎ} x c$
166	165 78	nfcsbw	$⊢ \underline{Ⅎ} x ⦋ c / i ⦌ ⦋ a / x ⦌ A$
167	83	csbeq2dv	$⊢ x = a \to ⦋ c / i ⦌ A = ⦋ c / i ⦌ ⦋ a / x ⦌ A$
168	164 166 167	cbvmpt	$⊢ (x \in X ⟼ ⦋ c / i ⦌ A) = (a \in X ⟼ ⦋ c / i ⦌ ⦋ a / x ⦌ A)$
169	168	oveq2i	$⊢ \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = \frac{d (a \in X⟼ ⦋ c / i ⦌ ⦋ a / x ⦌ A)}{d_{S} a}$
170		nfcv	$⊢ \underline{Ⅎ} a ⦋ c / i ⦌ B$
171	165 99	nfcsbw	$⊢ \underline{Ⅎ} x ⦋ c / i ⦌ ⦋ a / x ⦌ B$
172	101	csbeq2dv	$⊢ x = a \to ⦋ c / i ⦌ B = ⦋ c / i ⦌ ⦋ a / x ⦌ B$
173	170 171 172	cbvmpt	$⊢ (x \in X ⟼ ⦋ c / i ⦌ B) = (a \in X ⟼ ⦋ c / i ⦌ ⦋ a / x ⦌ B)$
174	163 169 173	3eqtr3g	$⊢ (φ \land c \in I) \to \frac{d (a \in X⟼ ⦋ c / i ⦌ ⦋ a / x ⦌ A)}{d_{S} a} = (a \in X ⟼ ⦋ c / i ⦌ ⦋ a / x ⦌ B)$
175	69 142 174	syl2anc	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to \frac{d (a \in X⟼ ⦋ c / i ⦌ ⦋ a / x ⦌ A)}{d_{S} a} = (a \in X ⟼ ⦋ c / i ⦌ ⦋ a / x ⦌ B)$
176	70 89 91 106 127 141 175	dvmptadd	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to \frac{d (a \in X⟼ \sum_{i \in b} ⦋ a / x ⦌ A + ⦋ c / i ⦌ ⦋ a / x ⦌ A)}{d_{S} a} = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ B + ⦋ c / i ⦌ ⦋ a / x ⦌ B)$
177		nfcv	$⊢ \underline{Ⅎ} a \sum_{i \in b \cup \{c\}} A$
178		nfcv	$⊢ \underline{Ⅎ} x (b \cup \{c\})$
179	178 78	nfsum	$⊢ \underline{Ⅎ} x \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ A$
180	83	sumeq2sdv	$⊢ x = a \to \sum_{i \in b \cup \{c\}} A = \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ A$
181	177 179 180	cbvmpt	$⊢ (x \in X ⟼ \sum_{i \in b \cup \{c\}} A) = (a \in X ⟼ \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ A)$
182		simpllr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \neg c \in b$
183		disjsn	$⊢ b \cap \{c\} = \emptyset \leftrightarrow \neg c \in b$
184	182 183	sylibr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to b \cap \{c\} = \emptyset$
185		eqidd	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to b \cup \{c\} = b \cup \{c\}$
186		simplr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to b \cup \{c\} \subseteq I$
187	71 186	ssfid	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to b \cup \{c\} \in Fin$
188		simp-4l	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in (b \cup \{c\})) \to φ$
189	186	sselda	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in (b \cup \{c\})) \to i \in I$
190		simplr	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in (b \cup \{c\})) \to a \in X$
191	188 189 190 86	syl3anc	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in (b \cup \{c\})) \to ⦋ a / x ⦌ A \in ℂ$
192	184 185 187 191	fsumsplit	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ A = \sum_{i \in b} ⦋ a / x ⦌ A + \sum_{i \in \{c\}} ⦋ a / x ⦌ A$
193		sumsns	$⊢ (c \in V \land ⦋ c / i ⦌ ⦋ a / x ⦌ A \in ℂ) \to \sum_{i \in \{c\}} ⦋ a / x ⦌ A = ⦋ c / i ⦌ ⦋ a / x ⦌ A$
194	111 126 193	sylancr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in \{c\}} ⦋ a / x ⦌ A = ⦋ c / i ⦌ ⦋ a / x ⦌ A$
195	194	oveq2d	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in b} ⦋ a / x ⦌ A + \sum_{i \in \{c\}} ⦋ a / x ⦌ A = \sum_{i \in b} ⦋ a / x ⦌ A + ⦋ c / i ⦌ ⦋ a / x ⦌ A$
196	192 195	eqtrd	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ A = \sum_{i \in b} ⦋ a / x ⦌ A + ⦋ c / i ⦌ ⦋ a / x ⦌ A$
197	196	mpteq2dva	$⊢ ((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \to (a \in X ⟼ \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ A) = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ A + ⦋ c / i ⦌ ⦋ a / x ⦌ A)$
198	181 197	syl5eq	$⊢ ((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \to (x \in X ⟼ \sum_{i \in b \cup \{c\}} A) = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ A + ⦋ c / i ⦌ ⦋ a / x ⦌ A)$
199	198	adantrr	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to (x \in X ⟼ \sum_{i \in b \cup \{c\}} A) = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ A + ⦋ c / i ⦌ ⦋ a / x ⦌ A)$
200	199	oveq2d	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = \frac{d (a \in X⟼ \sum_{i \in b} ⦋ a / x ⦌ A + ⦋ c / i ⦌ ⦋ a / x ⦌ A)}{d_{S} a}$
201		nfcv	$⊢ \underline{Ⅎ} a \sum_{i \in b \cup \{c\}} B$
202	178 99	nfsum	$⊢ \underline{Ⅎ} x \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ B$
203	101	sumeq2sdv	$⊢ x = a \to \sum_{i \in b \cup \{c\}} B = \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ B$
204	201 202 203	cbvmpt	$⊢ (x \in X ⟼ \sum_{i \in b \cup \{c\}} B) = (a \in X ⟼ \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ B)$
205	77 131	nfim	$⊢ Ⅎ x ((φ \land i \in I \land a \in X) \to ⦋ a / x ⦌ B \in ℂ)$
206	82 134	imbi12d	$⊢ x = a \to (((φ \land i \in I \land x \in X) \to B \in ℂ) \leftrightarrow ((φ \land i \in I \land a \in X) \to ⦋ a / x ⦌ B \in ℂ))$
207	205 206 7	chvarfv	$⊢ (φ \land i \in I \land a \in X) \to ⦋ a / x ⦌ B \in ℂ$
208	188 189 190 207	syl3anc	$⊢ ((((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \land i \in (b \cup \{c\})) \to ⦋ a / x ⦌ B \in ℂ$
209	184 185 187 208	fsumsplit	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ B = \sum_{i \in b} ⦋ a / x ⦌ B + \sum_{i \in \{c\}} ⦋ a / x ⦌ B$
210		sumsns	$⊢ (c \in V \land ⦋ c / i ⦌ ⦋ a / x ⦌ B \in ℂ) \to \sum_{i \in \{c\}} ⦋ a / x ⦌ B = ⦋ c / i ⦌ ⦋ a / x ⦌ B$
211	111 140 210	sylancr	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in \{c\}} ⦋ a / x ⦌ B = ⦋ c / i ⦌ ⦋ a / x ⦌ B$
212	211	oveq2d	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in b} ⦋ a / x ⦌ B + \sum_{i \in \{c\}} ⦋ a / x ⦌ B = \sum_{i \in b} ⦋ a / x ⦌ B + ⦋ c / i ⦌ ⦋ a / x ⦌ B$
213	209 212	eqtrd	$⊢ (((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \land a \in X) \to \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ B = \sum_{i \in b} ⦋ a / x ⦌ B + ⦋ c / i ⦌ ⦋ a / x ⦌ B$
214	213	mpteq2dva	$⊢ ((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \to (a \in X ⟼ \sum_{i \in b \cup \{c\}} ⦋ a / x ⦌ B) = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ B + ⦋ c / i ⦌ ⦋ a / x ⦌ B)$
215	204 214	syl5eq	$⊢ ((φ \land \neg c \in b) \land b \cup \{c\} \subseteq I) \to (x \in X ⟼ \sum_{i \in b \cup \{c\}} B) = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ B + ⦋ c / i ⦌ ⦋ a / x ⦌ B)$
216	215	adantrr	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to (x \in X ⟼ \sum_{i \in b \cup \{c\}} B) = (a \in X ⟼ \sum_{i \in b} ⦋ a / x ⦌ B + ⦋ c / i ⦌ ⦋ a / x ⦌ B)$
217	176 200 216	3eqtr4d	$⊢ ((φ \land \neg c \in b) \land (b \cup \{c\} \subseteq I \land \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B)$
218	217	exp32	$⊢ (φ \land \neg c \in b) \to (b \cup \{c\} \subseteq I \to (\frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B) \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B)))$
219	218	a2d	$⊢ (φ \land \neg c \in b) \to ((b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B)) \to (b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B)))$
220	68 219	syl5	$⊢ (φ \land \neg c \in b) \to ((b \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B)) \to (b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B)))$
221	220	expcom	$⊢ \neg c \in b \to (φ \to ((b \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B)) \to (b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B))))$
222	221	adantl	$⊢ (b \in Fin \land \neg c \in b) \to (φ \to ((b \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B)) \to (b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B))))$
223	222	a2d	$⊢ (b \in Fin \land \neg c \in b) \to ((φ \to (b \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b} B))) \to (φ \to (b \cup \{c\} \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in b \cup \{c\}} B))))$
224	18 27 36 45 64 223	findcard2s	$⊢ I \in Fin \to (φ \to (I \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in I} B)))$
225	5 224	mpcom	$⊢ φ \to (I \subseteq I \to \frac{d (x \in X⟼ \sum_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in I} B))$
226	9 225	mpi	$⊢ φ \to \frac{d (x \in X⟼ \sum_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{i \in I} B)$

Metamath Proof Explorer

Theorem dvmptfsum

Proof