Theorem dvmptfsum 15577

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

Hypotheses

Ref	Expression
dvmptfsum.j	⊢ 𝐽 = (𝐾 ↾t 𝑆)
dvmptfsum.k	⊢ 𝐾 = (TopOpen‘ℂfld)
dvmptfsum.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
dvmptfsum.x	⊢ (𝜑 → 𝑋 ∈ 𝐽)
dvmptfsum.i	⊢ (𝜑 → 𝐼 ∈ Fin)
dvmptfsum.a	⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)
dvmptfsum.b	⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)
dvmptfsum.d	⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))

Assertion

Ref	Expression
dvmptfsum	⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))

Distinct variable groups:   𝑥,𝑖,𝐼   𝜑,𝑖,𝑥   𝑆,𝑖,𝑥   𝑖,𝑋,𝑥

Allowed substitution hints:   𝐴(𝑥,𝑖)   𝐵(𝑥,𝑖)   𝐽(𝑥,𝑖)   𝐾(𝑥,𝑖)

Proof of Theorem dvmptfsum

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 3257	. 2 ⊢ 𝐼 ⊆ 𝐼
2		dvmptfsum.i	. . 3 ⊢ (𝜑 → 𝐼 ∈ Fin)
3		sseq1 3260	. . . . . 6 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐼 ↔ ∅ ⊆ 𝐼))
4		sumeq1 12033	. . . . . . . . 9 ⊢ (𝑎 = ∅ → Σ𝑖 ∈ 𝑎 𝐴 = Σ𝑖 ∈ ∅ 𝐴)
5	4	mpteq2dv 4200	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴))
6	5	oveq2d 6065	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)))
7		sumeq1 12033	. . . . . . . 8 ⊢ (𝑎 = ∅ → Σ𝑖 ∈ 𝑎 𝐵 = Σ𝑖 ∈ ∅ 𝐵)
8	7	mpteq2dv 4200	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))
9	6, 8	eqeq12d 2247	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵) ↔ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))
10	3, 9	imbi12d 234	. . . . 5 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵)) ↔ (∅ ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))))
11	10	imbi2d 230	. . . 4 ⊢ (𝑎 = ∅ → ((𝜑 → (𝑎 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵))) ↔ (𝜑 → (∅ ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))))
12		sseq1 3260	. . . . . 6 ⊢ (𝑎 = 𝑏 → (𝑎 ⊆ 𝐼 ↔ 𝑏 ⊆ 𝐼))
13		sumeq1 12033	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → Σ𝑖 ∈ 𝑎 𝐴 = Σ𝑖 ∈ 𝑏 𝐴)
14	13	mpteq2dv 4200	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴))
15	14	oveq2d 6065	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)))
16		sumeq1 12033	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → Σ𝑖 ∈ 𝑎 𝐵 = Σ𝑖 ∈ 𝑏 𝐵)
17	16	mpteq2dv 4200	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))
18	15, 17	eqeq12d 2247	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵) ↔ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵)))
19	12, 18	imbi12d 234	. . . . 5 ⊢ (𝑎 = 𝑏 → ((𝑎 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵)) ↔ (𝑏 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))))
20	19	imbi2d 230	. . . 4 ⊢ (𝑎 = 𝑏 → ((𝜑 → (𝑎 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵))) ↔ (𝜑 → (𝑏 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵)))))
21		sseq1 3260	. . . . . 6 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ⊆ 𝐼 ↔ (𝑏 ∪ {𝑐}) ⊆ 𝐼))
22		sumeq1 12033	. . . . . . . . 9 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑖 ∈ 𝑎 𝐴 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)
23	22	mpteq2dv 4200	. . . . . . . 8 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴))
24	23	oveq2d 6065	. . . . . . 7 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)))
25		sumeq1 12033	. . . . . . . 8 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑖 ∈ 𝑎 𝐵 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)
26	25	mpteq2dv 4200	. . . . . . 7 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))
27	24, 26	eqeq12d 2247	. . . . . 6 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵) ↔ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))
28	21, 27	imbi12d 234	. . . . 5 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵)) ↔ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
29	28	imbi2d 230	. . . 4 ⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ((𝜑 → (𝑎 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵))) ↔ (𝜑 → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
30		sseq1 3260	. . . . . 6 ⊢ (𝑎 = 𝐼 → (𝑎 ⊆ 𝐼 ↔ 𝐼 ⊆ 𝐼))
31		sumeq1 12033	. . . . . . . . 9 ⊢ (𝑎 = 𝐼 → Σ𝑖 ∈ 𝑎 𝐴 = Σ𝑖 ∈ 𝐼 𝐴)
32	31	mpteq2dv 4200	. . . . . . . 8 ⊢ (𝑎 = 𝐼 → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴))
33	32	oveq2d 6065	. . . . . . 7 ⊢ (𝑎 = 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)))
34		sumeq1 12033	. . . . . . . 8 ⊢ (𝑎 = 𝐼 → Σ𝑖 ∈ 𝑎 𝐵 = Σ𝑖 ∈ 𝐼 𝐵)
35	34	mpteq2dv 4200	. . . . . . 7 ⊢ (𝑎 = 𝐼 → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))
36	33, 35	eqeq12d 2247	. . . . . 6 ⊢ (𝑎 = 𝐼 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵) ↔ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵)))
37	30, 36	imbi12d 234	. . . . 5 ⊢ (𝑎 = 𝐼 → ((𝑎 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵)) ↔ (𝐼 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))))
38	37	imbi2d 230	. . . 4 ⊢ (𝑎 = 𝐼 → ((𝜑 → (𝑎 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑎 𝐵))) ↔ (𝜑 → (𝐼 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵)))))
39		dvmptfsum.s	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
40		dvmptfsum.j	. . . . . . . 8 ⊢ 𝐽 = (𝐾 ↾t 𝑆)
41		dvmptfsum.k	. . . . . . . . 9 ⊢ 𝐾 = (TopOpen‘ℂfld)
42	41	cnfldtopn 15391	. . . . . . . 8 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
43		dvmptfsum.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐽)
44		0cnd 8263	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℂ)
45	39, 40, 42, 43, 44	dvconstss 15550	. . . . . . 7 ⊢ (𝜑 → (𝑆 D (𝑋 × {0})) = (𝑋 × {0}))
46		fconstmpt 4796	. . . . . . . 8 ⊢ (𝑋 × {0}) = (𝑥 ∈ 𝑋 ↦ 0)
47	46	oveq2i 6060	. . . . . . 7 ⊢ (𝑆 D (𝑋 × {0})) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 0))
48	45, 47, 46	3eqtr3g 2288	. . . . . 6 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 0)) = (𝑥 ∈ 𝑋 ↦ 0))
49		sum0 12067	. . . . . . . 8 ⊢ Σ𝑖 ∈ ∅ 𝐴 = 0
50	49	mpteq2i 4196	. . . . . . 7 ⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴) = (𝑥 ∈ 𝑋 ↦ 0)
51	50	oveq2i 6060	. . . . . 6 ⊢ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 0))
52		sum0 12067	. . . . . . 7 ⊢ Σ𝑖 ∈ ∅ 𝐵 = 0
53	52	mpteq2i 4196	. . . . . 6 ⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵) = (𝑥 ∈ 𝑋 ↦ 0)
54	48, 51, 53	3eqtr4g 2290	. . . . 5 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))
55	54	a1d 22	. . . 4 ⊢ (𝜑 → (∅ ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))
56		ssun1 3381	. . . . . . . . 9 ⊢ 𝑏 ⊆ (𝑏 ∪ {𝑐})
57		sstr 3245	. . . . . . . . 9 ⊢ ((𝑏 ⊆ (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → 𝑏 ⊆ 𝐼)
58	56, 57	mpan 424	. . . . . . . 8 ⊢ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → 𝑏 ⊆ 𝐼)
59	58	imim1i 60	. . . . . . 7 ⊢ ((𝑏 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵)))
60	39	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → 𝑆 ∈ {ℝ, ℂ})
61		simprl 531	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) → 𝑏 ∈ Fin)
62	61	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → 𝑏 ∈ Fin)
63		simp-4l 543	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ 𝑏) → 𝜑)
64	58	ad2antlr 489	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → 𝑏 ⊆ 𝐼)
65	64	sselda 3237	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ 𝑏) → 𝑖 ∈ 𝐼)
66		simplr 529	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ 𝑏) → 𝑎 ∈ 𝑋)
67		nfv 1577	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋)
68		nfcsb1v 3170	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐴
69	68	nfel1 2395	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ
70	67, 69	nfim 1621	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
71		eleq1w 2293	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝑋 ↔ 𝑎 ∈ 𝑋))
72	71	3anbi3d 1355	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) ↔ (𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋)))
73		csbeq1a 3146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑎 → 𝐴 = ⦋𝑎 / 𝑥⦌𝐴)
74	73	eleq1d 2301	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → (𝐴 ∈ ℂ ↔ ⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ))
75	72, 74	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)))
76		dvmptfsum.a	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)
77	70, 75, 76	chvarfv 1748	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
78	63, 65, 66, 77	syl3anc 1274	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ 𝑏) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
79	62, 78	fsumcl 12079	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
80	79	adantlrr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
81		nfcsb1v 3170	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐵
82	81	nfel1 2395	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ
83	67, 82	nfim 1621	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋) → ⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
84		csbeq1a 3146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑎 → 𝐵 = ⦋𝑎 / 𝑥⦌𝐵)
85	84	eleq1d 2301	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → (𝐵 ∈ ℂ ↔ ⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ))
86	72, 85	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋) → ⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)))
87		dvmptfsum.b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ℂ)
88	83, 86, 87	chvarfv 1748	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋) → ⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
89	63, 65, 66, 88	syl3anc 1274	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ 𝑏) → ⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
90	62, 89	fsumcl 12079	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
91	90	adantlrr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
92		nfcv 2384	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎Σ𝑖 ∈ 𝑏 𝐴
93		nfcv 2384	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑏
94	93, 68	nfsum 12035	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴
95	73	sumeq2sdv 12048	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → Σ𝑖 ∈ 𝑏 𝐴 = Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴)
96	92, 94, 95	cbvmpt 4204	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴) = (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴)
97	96	oveq2i 6060	. . . . . . . . . . . . . 14 ⊢ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑆 D (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴))
98		nfcv 2384	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎Σ𝑖 ∈ 𝑏 𝐵
99	93, 81	nfsum 12035	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵
100	84	sumeq2sdv 12048	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → Σ𝑖 ∈ 𝑏 𝐵 = Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵)
101	98, 99, 100	cbvmpt 4204	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵) = (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵)
102	97, 101	eqeq12i 2246	. . . . . . . . . . . . 13 ⊢ ((𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵) ↔ (𝑆 D (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴)) = (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵))
103	102	biimpi 120	. . . . . . . . . . . 12 ⊢ ((𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵) → (𝑆 D (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴)) = (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵))
104	103	ad2antll 491	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝑆 D (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴)) = (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵))
105	41	cnfldtopon 15392	. . . . . . . . . . . . . . 15 ⊢ 𝐾 ∈ (TopOn‘ℂ)
106		recnprss 15539	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
107	39, 106	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
108		resttopon 15023	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆))
109	105, 107, 108	sylancr 414	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆))
110	40, 109	eqeltrid 2319	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑆))
111		toponss 14878	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑆) ∧ 𝑋 ∈ 𝐽) → 𝑋 ⊆ 𝑆)
112	110, 43, 111	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
113	112	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → 𝑋 ⊆ 𝑆)
114		simpr 110	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏) → ¬ 𝑐 ∈ 𝑏)
115	114	anim2i 342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) → (𝜑 ∧ ¬ 𝑐 ∈ 𝑏))
116		simplll 535	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → 𝜑)
117		ssun2 3382	. . . . . . . . . . . . . . . . 17 ⊢ {𝑐} ⊆ (𝑏 ∪ {𝑐})
118		sstr 3245	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑐} ⊆ (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → {𝑐} ⊆ 𝐼)
119	117, 118	mpan 424	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → {𝑐} ⊆ 𝐼)
120		vex 2815	. . . . . . . . . . . . . . . . 17 ⊢ 𝑐 ∈ V
121	120	snss 3828	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝐼 ↔ {𝑐} ⊆ 𝐼)
122	119, 121	sylibr 134	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → 𝑐 ∈ 𝐼)
123	122	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → 𝑐 ∈ 𝐼)
124		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ 𝑋)
125	76	3expb 1231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) → 𝐴 ∈ ℂ)
126	125	ancom2s 568	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑖 ∈ 𝐼)) → 𝐴 ∈ ℂ)
127	126	ralrimivva 2624	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑖 ∈ 𝐼 𝐴 ∈ ℂ)
128		nfcsb1v 3170	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴
129	128	nfel1 2395	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ
130		csbeq1a 3146	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑐 → ⦋𝑎 / 𝑥⦌𝐴 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)
131	130	eleq1d 2301	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑐 → (⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ ↔ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ))
132	69, 129, 74, 131	rspc2 2931	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝐼) → (∀𝑥 ∈ 𝑋 ∀𝑖 ∈ 𝐼 𝐴 ∈ ℂ → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ))
133	132	ancoms 268	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑖 ∈ 𝐼 𝐴 ∈ ℂ → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ))
134	127, 133	mpan9 281	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋)) → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
135	116, 123, 124, 134	syl12anc 1272	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
136	135	adantlrr 483	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) ∧ 𝑎 ∈ 𝑋) → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
137	115, 136	sylanl1 402	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) ∧ 𝑎 ∈ 𝑋) → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
138	87	3expb 1231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) → 𝐵 ∈ ℂ)
139	138	ancom2s 568	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑖 ∈ 𝐼)) → 𝐵 ∈ ℂ)
140	139	ralrimivva 2624	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑖 ∈ 𝐼 𝐵 ∈ ℂ)
141		nfcsb1v 3170	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵
142	141	nfel1 2395	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ
143		csbeq1a 3146	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑐 → ⦋𝑎 / 𝑥⦌𝐵 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)
144	143	eleq1d 2301	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑐 → (⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ ↔ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ))
145	82, 142, 85, 144	rspc2 2931	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝐼) → (∀𝑥 ∈ 𝑋 ∀𝑖 ∈ 𝐼 𝐵 ∈ ℂ → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ))
146	145	ancoms 268	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑖 ∈ 𝐼 𝐵 ∈ ℂ → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ))
147	140, 146	mpan9 281	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋)) → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
148	116, 123, 124, 147	syl12anc 1272	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
149	148	adantlrr 483	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) ∧ 𝑎 ∈ 𝑋) → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
150	115, 149	sylanl1 402	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) ∧ 𝑎 ∈ 𝑋) → ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
151		simpll 527	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → 𝜑)
152	122	ad2antrl 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → 𝑐 ∈ 𝐼)
153		nfv 1577	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑐 ∈ 𝐼)
154		nfcv 2384	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑆
155		nfcv 2384	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖 D
156		nfcv 2384	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖𝑋
157		nfcsb1v 3170	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖⦋𝑐 / 𝑖⦌𝐴
158	156, 157	nfmpt 4201	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴)
159	154, 155, 158	nfov 6079	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖(𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴))
160		nfcsb1v 3170	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖⦋𝑐 / 𝑖⦌𝐵
161	156, 160	nfmpt 4201	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖(𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐵)
162	159, 161	nfeq 2392	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴)) = (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐵)
163	153, 162	nfim 1621	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴)) = (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐵))
164		eleq1w 2293	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑐 → (𝑖 ∈ 𝐼 ↔ 𝑐 ∈ 𝐼))
165	164	anbi2d 464	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑐 → ((𝜑 ∧ 𝑖 ∈ 𝐼) ↔ (𝜑 ∧ 𝑐 ∈ 𝐼)))
166		csbeq1a 3146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑐 → 𝐴 = ⦋𝑐 / 𝑖⦌𝐴)
167	166	mpteq2dv 4200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑐 → (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴))
168	167	oveq2d 6065	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑐 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴)))
169		csbeq1a 3146	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑐 → 𝐵 = ⦋𝑐 / 𝑖⦌𝐵)
170	169	mpteq2dv 4200	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑐 → (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐵))
171	168, 170	eqeq12d 2247	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑐 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵) ↔ (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴)) = (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐵)))
172	165, 171	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑐 → (((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ↔ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴)) = (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐵))))
173		dvmptfsum.d	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 𝐵))
174	163, 172, 173	chvarfv 1748	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴)) = (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐵))
175		nfcv 2384	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎⦋𝑐 / 𝑖⦌𝐴
176		nfcv 2384	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑐
177	176, 68	nfcsbw 3174	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴
178	73	csbeq2dv 3163	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → ⦋𝑐 / 𝑖⦌𝐴 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)
179	175, 177, 178	cbvmpt 4204	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴) = (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)
180	179	oveq2i 6060	. . . . . . . . . . . . . 14 ⊢ (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐴)) = (𝑆 D (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴))
181		nfcv 2384	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎⦋𝑐 / 𝑖⦌𝐵
182	176, 81	nfcsbw 3174	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵
183	84	csbeq2dv 3163	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → ⦋𝑐 / 𝑖⦌𝐵 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)
184	181, 182, 183	cbvmpt 4204	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌𝐵) = (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)
185	174, 180, 184	3eqtr3g 2288	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑆 D (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)) = (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵))
186	151, 152, 185	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝑆 D (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)) = (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵))
187	115, 186	sylan 283	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝑆 D (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)) = (𝑎 ∈ 𝑋 ↦ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵))
188	60, 80, 91, 104, 113, 137, 150, 187	dvmptaddx 15571	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝑆 D (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴))) = (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)))
189		nfcv 2384	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑎Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴
190		nfcv 2384	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑏 ∪ {𝑐})
191	190, 68	nfsum 12035	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐴
192	73	sumeq2sdv 12048	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐴)
193	189, 191, 192	cbvmpt 4204	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐴)
194		simpllr 536	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → ¬ 𝑐 ∈ 𝑏)
195		disjsn 3750	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∩ {𝑐}) = ∅ ↔ ¬ 𝑐 ∈ 𝑏)
196	194, 195	sylibr 134	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → (𝑏 ∩ {𝑐}) = ∅)
197	115, 196	sylanl1 402	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → (𝑏 ∩ {𝑐}) = ∅)
198		eqidd 2233	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → (𝑏 ∪ {𝑐}) = (𝑏 ∪ {𝑐}))
199	120	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → 𝑐 ∈ V)
200	115, 194	sylanl1 402	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → ¬ 𝑐 ∈ 𝑏)
201		unsnfi 7178	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ Fin ∧ 𝑐 ∈ V ∧ ¬ 𝑐 ∈ 𝑏) → (𝑏 ∪ {𝑐}) ∈ Fin)
202	62, 199, 200, 201	syl3anc 1274	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → (𝑏 ∪ {𝑐}) ∈ Fin)
203		simp-4l 543	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝜑)
204		simplr 529	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → (𝑏 ∪ {𝑐}) ⊆ 𝐼)
205	204	sselda 3237	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑖 ∈ 𝐼)
206		simplr 529	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑎 ∈ 𝑋)
207	203, 205, 206, 77	syl3anc 1274	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → ⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ)
208	197, 198, 202, 207	fsumsplit 12086	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐴 = (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐴))
209		sumsns 12094	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ V ∧ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴 ∈ ℂ) → Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐴 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)
210	120, 135, 209	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐴 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)
211	115, 210	sylanl1 402	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐴 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)
212	211	oveq2d 6065	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐴) = (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴))
213	208, 212	eqtrd 2265	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐴 = (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴))
214	213	mpteq2dva 4199	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐴) = (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)))
215	193, 214	eqtrid 2277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)))
216	215	adantrr 479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴)))
217	216	oveq2d 6065	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑆 D (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐴 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐴))))
218		nfcv 2384	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑎Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵
219	190, 81	nfsum 12035	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐵
220	84	sumeq2sdv 12048	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐵)
221	218, 219, 220	cbvmpt 4204	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐵)
222	203, 205, 206, 88	syl3anc 1274	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → ⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ)
223	197, 198, 202, 222	fsumsplit 12086	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐵 = (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐵))
224		sumsns 12094	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ V ∧ ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵 ∈ ℂ) → Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐵 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)
225	120, 148, 224	sylancr 414	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐵 = ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)
226	225	oveq2d 6065	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐵) = (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵))
227	115, 226	sylanl1 402	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + Σ𝑖 ∈ {𝑐}⦋𝑎 / 𝑥⦌𝐵) = (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵))
228	223, 227	eqtrd 2265	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎 ∈ 𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐵 = (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵))
229	228	mpteq2dva 4199	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑎 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})⦋𝑎 / 𝑥⦌𝐵) = (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)))
230	221, 229	eqtrid 2277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)))
231	230	adantrr 479	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎 ∈ 𝑋 ↦ (Σ𝑖 ∈ 𝑏 ⦋𝑎 / 𝑥⦌𝐵 + ⦋𝑐 / 𝑖⦌⦋𝑎 / 𝑥⦌𝐵)))
232	188, 217, 231	3eqtr4d 2275	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))
233	232	exp32 365	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → ((𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵) → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
234	233	a2d 26	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) → (((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
235	59, 234	syl5 32	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏)) → ((𝑏 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
236	235	expcom 116	. . . . 5 ⊢ ((𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏) → (𝜑 → ((𝑏 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
237	236	a2d 26	. . . 4 ⊢ ((𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏) → ((𝜑 → (𝑏 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝑏 𝐵))) → (𝜑 → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
238	11, 20, 29, 38, 55, 237	findcard2s 7146	. . 3 ⊢ (𝐼 ∈ Fin → (𝜑 → (𝐼 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))))
239	2, 238	mpcom 36	. 2 ⊢ (𝜑 → (𝐼 ⊆ 𝐼 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵)))
240	1, 239	mpi 15	1 ⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ 𝐼 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∧ w3a 1005   = wceq 1398   ∈ wcel 2203  ∀wral 2520  Vcvv 2812  ⦋csb 3137   ∪ cun 3208   ∩ cin 3209   ⊆ wss 3210  ∅c0 3507  {csn 3688  {cpr 3689   ↦ cmpt 4170   × cxp 4746  ‘cfv 5351  (class class class)co 6049  Fincfn 6974  ℂcc 8121  ℝcr 8122  0cc0 8123   + caddc 8126  Σcsu 12031   ↾_t crest 13441  TopOpenctopn 13442  ℂ_fldccnfld 14691  TopOnctopon 14862   D cdv 15507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4224  ax-sep 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-iinf 4709  ax-cnex 8214  ax-resscn 8215  ax-1cn 8216  ax-1re 8217  ax-icn 8218  ax-addcl 8219  ax-addrcl 8220  ax-mulcl 8221  ax-mulrcl 8222  ax-addcom 8223  ax-mulcom 8224  ax-addass 8225  ax-mulass 8226  ax-distr 8227  ax-i2m1 8228  ax-0lt1 8229  ax-1rid 8230  ax-0id 8231  ax-rnegex 8232  ax-precex 8233  ax-cnre 8234  ax-pre-ltirr 8235  ax-pre-ltwlin 8236  ax-pre-lttrn 8237  ax-pre-apti 8238  ax-pre-ltadd 8239  ax-pre-mulgt0 8240  ax-pre-mulext 8241  ax-arch 8242  ax-caucvg 8243  ax-addf 8245

This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rmo 2528  df-rab 2529  df-v 2814  df-sbc 3042  df-csb 3138  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-if 3620  df-pw 3670  df-sn 3694  df-pr 3695  df-tp 3696  df-op 3697  df-uni 3914  df-int 3949  df-iun 3992  df-br 4109  df-opab 4171  df-mpt 4172  df-tr 4208  df-id 4413  df-po 4416  df-iso 4417  df-iord 4486  df-on 4488  df-ilim 4489  df-suc 4491  df-iom 4712  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-iota 5311  df-fun 5353  df-fn 5354  df-f 5355  df-f1 5356  df-fo 5357  df-f1o 5358  df-fv 5359  df-isom 5360  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-of 6265  df-1st 6333  df-2nd 6334  df-recs 6535  df-irdg 6600  df-frec 6621  df-1o 6646  df-oadd 6650  df-er 6766  df-map 6883  df-pm 6884  df-en 6975  df-dom 6976  df-fin 6977  df-sup 7274  df-inf 7275  df-pnf 8306  df-mnf 8307  df-xr 8308  df-ltxr 8309  df-le 8310  df-sub 8442  df-neg 8443  df-reap 8845  df-ap 8852  df-div 8943  df-inn 9234  df-2 9292  df-3 9293  df-4 9294  df-5 9295  df-6 9296  df-7 9297  df-8 9298  df-9 9299  df-n0 9493  df-z 9574  df-dec 9706  df-uz 9850  df-q 9948  df-rp 9983  df-xneg 10101  df-xadd 10102  df-fz 10339  df-fzo 10473  df-seqfrec 10806  df-exp 10897  df-ihash 11134  df-cj 11520  df-re 11521  df-im 11522  df-rsqrt 11676  df-abs 11677  df-clim 11957  df-sumdc 12032  df-struct 13203  df-ndx 13204  df-slot 13205  df-base 13207  df-plusg 13292  df-mulr 13293  df-starv 13294  df-tset 13298  df-ple 13299  df-ds 13301  df-unif 13302  df-rest 13443  df-topn 13444  df-topgen 13462  df-psmet 14678  df-xmet 14679  df-met 14680  df-bl 14681  df-mopn 14682  df-fg 14684  df-metu 14685  df-cnfld 14692  df-top 14850  df-topon 14863  df-topsp 14883  df-bases 14895  df-ntr 14948  df-cn 15040  df-cnp 15041  df-tx 15105  df-xms 15191  df-ms 15192  df-cncf 15423  df-limced 15508  df-dvap 15509

This theorem is referenced by:  dvply1  15617