MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvmptfsum Structured version   Visualization version   GIF version

Theorem dvmptfsum 25339
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.
StepHypRef Expression
1 ssid 3966 . 2 𝐼𝐼
2 dvmptfsum.i . . 3 (𝜑𝐼 ∈ Fin)
3 sseq1 3969 . . . . . 6 (𝑎 = ∅ → (𝑎𝐼 ↔ ∅ ⊆ 𝐼))
4 sumeq1 15573 . . . . . . . . 9 (𝑎 = ∅ → Σ𝑖𝑎 𝐴 = Σ𝑖 ∈ ∅ 𝐴)
54mpteq2dv 5207 . . . . . . . 8 (𝑎 = ∅ → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴))
65oveq2d 7373 . . . . . . 7 (𝑎 = ∅ → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)))
7 sumeq1 15573 . . . . . . . 8 (𝑎 = ∅ → Σ𝑖𝑎 𝐵 = Σ𝑖 ∈ ∅ 𝐵)
87mpteq2dv 5207 . . . . . . 7 (𝑎 = ∅ → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))
96, 8eqeq12d 2752 . . . . . 6 (𝑎 = ∅ → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) ↔ (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))
103, 9imbi12d 344 . . . . 5 (𝑎 = ∅ → ((𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵)) ↔ (∅ ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))))
1110imbi2d 340 . . . 4 (𝑎 = ∅ → ((𝜑 → (𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵))) ↔ (𝜑 → (∅ ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))))
12 sseq1 3969 . . . . . 6 (𝑎 = 𝑏 → (𝑎𝐼𝑏𝐼))
13 sumeq1 15573 . . . . . . . . 9 (𝑎 = 𝑏 → Σ𝑖𝑎 𝐴 = Σ𝑖𝑏 𝐴)
1413mpteq2dv 5207 . . . . . . . 8 (𝑎 = 𝑏 → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴))
1514oveq2d 7373 . . . . . . 7 (𝑎 = 𝑏 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)))
16 sumeq1 15573 . . . . . . . 8 (𝑎 = 𝑏 → Σ𝑖𝑎 𝐵 = Σ𝑖𝑏 𝐵)
1716mpteq2dv 5207 . . . . . . 7 (𝑎 = 𝑏 → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))
1815, 17eqeq12d 2752 . . . . . 6 (𝑎 = 𝑏 → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) ↔ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)))
1912, 18imbi12d 344 . . . . 5 (𝑎 = 𝑏 → ((𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵)) ↔ (𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))))
2019imbi2d 340 . . . 4 (𝑎 = 𝑏 → ((𝜑 → (𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵))) ↔ (𝜑 → (𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)))))
21 sseq1 3969 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎𝐼 ↔ (𝑏 ∪ {𝑐}) ⊆ 𝐼))
22 sumeq1 15573 . . . . . . . . 9 (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑖𝑎 𝐴 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)
2322mpteq2dv 5207 . . . . . . . 8 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴))
2423oveq2d 7373 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)))
25 sumeq1 15573 . . . . . . . 8 (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑖𝑎 𝐵 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)
2625mpteq2dv 5207 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))
2724, 26eqeq12d 2752 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) ↔ (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))
2821, 27imbi12d 344 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵)) ↔ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
2928imbi2d 340 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝜑 → (𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵))) ↔ (𝜑 → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
30 sseq1 3969 . . . . . 6 (𝑎 = 𝐼 → (𝑎𝐼𝐼𝐼))
31 sumeq1 15573 . . . . . . . . 9 (𝑎 = 𝐼 → Σ𝑖𝑎 𝐴 = Σ𝑖𝐼 𝐴)
3231mpteq2dv 5207 . . . . . . . 8 (𝑎 = 𝐼 → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴))
3332oveq2d 7373 . . . . . . 7 (𝑎 = 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)))
34 sumeq1 15573 . . . . . . . 8 (𝑎 = 𝐼 → Σ𝑖𝑎 𝐵 = Σ𝑖𝐼 𝐵)
3534mpteq2dv 5207 . . . . . . 7 (𝑎 = 𝐼 → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵))
3633, 35eqeq12d 2752 . . . . . 6 (𝑎 = 𝐼 → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) ↔ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵)))
3730, 36imbi12d 344 . . . . 5 (𝑎 = 𝐼 → ((𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵)) ↔ (𝐼𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵))))
3837imbi2d 340 . . . 4 (𝑎 = 𝐼 → ((𝜑 → (𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵))) ↔ (𝜑 → (𝐼𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵)))))
39 dvmptfsum.s . . . . . . 7 (𝜑𝑆 ∈ {ℝ, ℂ})
40 0cnd 11148 . . . . . . 7 ((𝜑𝑥𝑆) → 0 ∈ ℂ)
41 0cnd 11148 . . . . . . . 8 (𝜑 → 0 ∈ ℂ)
4239, 41dvmptc 25322 . . . . . . 7 (𝜑 → (𝑆 D (𝑥𝑆 ↦ 0)) = (𝑥𝑆 ↦ 0))
43 dvmptfsum.j . . . . . . . . 9 𝐽 = (𝐾t 𝑆)
44 dvmptfsum.k . . . . . . . . . . 11 𝐾 = (TopOpen‘ℂfld)
4544cnfldtopon 24146 . . . . . . . . . 10 𝐾 ∈ (TopOn‘ℂ)
46 recnprss 25268 . . . . . . . . . . 11 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
4739, 46syl 17 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℂ)
48 resttopon 22512 . . . . . . . . . 10 ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾t 𝑆) ∈ (TopOn‘𝑆))
4945, 47, 48sylancr 587 . . . . . . . . 9 (𝜑 → (𝐾t 𝑆) ∈ (TopOn‘𝑆))
5043, 49eqeltrid 2842 . . . . . . . 8 (𝜑𝐽 ∈ (TopOn‘𝑆))
51 dvmptfsum.x . . . . . . . 8 (𝜑𝑋𝐽)
52 toponss 22276 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑆) ∧ 𝑋𝐽) → 𝑋𝑆)
5350, 51, 52syl2anc 584 . . . . . . 7 (𝜑𝑋𝑆)
5439, 40, 40, 42, 53, 43, 44, 51dvmptres 25327 . . . . . 6 (𝜑 → (𝑆 D (𝑥𝑋 ↦ 0)) = (𝑥𝑋 ↦ 0))
55 sum0 15606 . . . . . . . 8 Σ𝑖 ∈ ∅ 𝐴 = 0
5655mpteq2i 5210 . . . . . . 7 (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴) = (𝑥𝑋 ↦ 0)
5756oveq2i 7368 . . . . . 6 (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑆 D (𝑥𝑋 ↦ 0))
58 sum0 15606 . . . . . . 7 Σ𝑖 ∈ ∅ 𝐵 = 0
5958mpteq2i 5210 . . . . . 6 (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵) = (𝑥𝑋 ↦ 0)
6054, 57, 593eqtr4g 2801 . . . . 5 (𝜑 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))
6160a1d 25 . . . 4 (𝜑 → (∅ ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))
62 ssun1 4132 . . . . . . . . . 10 𝑏 ⊆ (𝑏 ∪ {𝑐})
63 sstr 3952 . . . . . . . . . 10 ((𝑏 ⊆ (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → 𝑏𝐼)
6462, 63mpan 688 . . . . . . . . 9 ((𝑏 ∪ {𝑐}) ⊆ 𝐼𝑏𝐼)
6564imim1i 63 . . . . . . . 8 ((𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)))
66 simpll 765 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → 𝜑)
6766, 39syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → 𝑆 ∈ {ℝ, ℂ})
682ad3antrrr 728 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝐼 ∈ Fin)
6964ad2antlr 725 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑏𝐼)
7068, 69ssfid 9211 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑏 ∈ Fin)
71 simp-4l 781 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖𝑏) → 𝜑)
7269sselda 3944 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖𝑏) → 𝑖𝐼)
73 simplr 767 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖𝑏) → 𝑎𝑋)
74 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑥(𝜑𝑖𝐼𝑎𝑋)
75 nfcsb1v 3880 . . . . . . . . . . . . . . . . . 18 𝑥𝑎 / 𝑥𝐴
7675nfel1 2923 . . . . . . . . . . . . . . . . 17 𝑥𝑎 / 𝑥𝐴 ∈ ℂ
7774, 76nfim 1899 . . . . . . . . . . . . . . . 16 𝑥((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐴 ∈ ℂ)
78 eleq1w 2820 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (𝑥𝑋𝑎𝑋))
79783anbi3d 1442 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → ((𝜑𝑖𝐼𝑥𝑋) ↔ (𝜑𝑖𝐼𝑎𝑋)))
80 csbeq1a 3869 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎𝐴 = 𝑎 / 𝑥𝐴)
8180eleq1d 2822 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝐴 ∈ ℂ ↔ 𝑎 / 𝑥𝐴 ∈ ℂ))
8279, 81imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (((𝜑𝑖𝐼𝑥𝑋) → 𝐴 ∈ ℂ) ↔ ((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐴 ∈ ℂ)))
83 dvmptfsum.a . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝐼𝑥𝑋) → 𝐴 ∈ ℂ)
8477, 82, 83chvarfv 2233 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐴 ∈ ℂ)
8571, 72, 73, 84syl3anc 1371 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖𝑏) → 𝑎 / 𝑥𝐴 ∈ ℂ)
8670, 85fsumcl 15618 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖𝑏 𝑎 / 𝑥𝐴 ∈ ℂ)
8786adantlrr 719 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) ∧ 𝑎𝑋) → Σ𝑖𝑏 𝑎 / 𝑥𝐴 ∈ ℂ)
88 sumex 15572 . . . . . . . . . . . . 13 Σ𝑖𝑏 𝑎 / 𝑥𝐵 ∈ V
8988a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) ∧ 𝑎𝑋) → Σ𝑖𝑏 𝑎 / 𝑥𝐵 ∈ V)
90 nfcv 2907 . . . . . . . . . . . . . . . . 17 𝑎Σ𝑖𝑏 𝐴
91 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑥𝑏
9291, 75nfsum 15575 . . . . . . . . . . . . . . . . 17 𝑥Σ𝑖𝑏 𝑎 / 𝑥𝐴
9380sumeq2sdv 15589 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → Σ𝑖𝑏 𝐴 = Σ𝑖𝑏 𝑎 / 𝑥𝐴)
9490, 92, 93cbvmpt 5216 . . . . . . . . . . . . . . . 16 (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴)
9594oveq2i 7368 . . . . . . . . . . . . . . 15 (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑆 D (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴))
96 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑎Σ𝑖𝑏 𝐵
97 nfcsb1v 3880 . . . . . . . . . . . . . . . . 17 𝑥𝑎 / 𝑥𝐵
9891, 97nfsum 15575 . . . . . . . . . . . . . . . 16 𝑥Σ𝑖𝑏 𝑎 / 𝑥𝐵
99 csbeq1a 3869 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎𝐵 = 𝑎 / 𝑥𝐵)
10099sumeq2sdv 15589 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → Σ𝑖𝑏 𝐵 = Σ𝑖𝑏 𝑎 / 𝑥𝐵)
10196, 98, 100cbvmpt 5216 . . . . . . . . . . . . . . 15 (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐵)
10295, 101eqeq12i 2754 . . . . . . . . . . . . . 14 ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵) ↔ (𝑆 D (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴)) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐵))
103102biimpi 215 . . . . . . . . . . . . 13 ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵) → (𝑆 D (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴)) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐵))
104103ad2antll 727 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴)) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐵))
105 simplll 773 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝜑)
106 ssun2 4133 . . . . . . . . . . . . . . . . 17 {𝑐} ⊆ (𝑏 ∪ {𝑐})
107 sstr 3952 . . . . . . . . . . . . . . . . 17 (({𝑐} ⊆ (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → {𝑐} ⊆ 𝐼)
108106, 107mpan 688 . . . . . . . . . . . . . . . 16 ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → {𝑐} ⊆ 𝐼)
109 vex 3449 . . . . . . . . . . . . . . . . 17 𝑐 ∈ V
110109snss 4746 . . . . . . . . . . . . . . . 16 (𝑐𝐼 ↔ {𝑐} ⊆ 𝐼)
111108, 110sylibr 233 . . . . . . . . . . . . . . 15 ((𝑏 ∪ {𝑐}) ⊆ 𝐼𝑐𝐼)
112111ad2antlr 725 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑐𝐼)
113 simpr 485 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑎𝑋)
114833expb 1120 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖𝐼𝑥𝑋)) → 𝐴 ∈ ℂ)
115114ancom2s 648 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑖𝐼)) → 𝐴 ∈ ℂ)
116115ralrimivva 3197 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝑋𝑖𝐼 𝐴 ∈ ℂ)
117 nfcsb1v 3880 . . . . . . . . . . . . . . . . . 18 𝑖𝑐 / 𝑖𝑎 / 𝑥𝐴
118117nfel1 2923 . . . . . . . . . . . . . . . . 17 𝑖𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ
119 csbeq1a 3869 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑐𝑎 / 𝑥𝐴 = 𝑐 / 𝑖𝑎 / 𝑥𝐴)
120119eleq1d 2822 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑎 / 𝑥𝐴 ∈ ℂ ↔ 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ))
12176, 118, 81, 120rspc2 3588 . . . . . . . . . . . . . . . 16 ((𝑎𝑋𝑐𝐼) → (∀𝑥𝑋𝑖𝐼 𝐴 ∈ ℂ → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ))
122121ancoms 459 . . . . . . . . . . . . . . 15 ((𝑐𝐼𝑎𝑋) → (∀𝑥𝑋𝑖𝐼 𝐴 ∈ ℂ → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ))
123116, 122mpan9 507 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝐼𝑎𝑋)) → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ)
124105, 112, 113, 123syl12anc 835 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ)
125124adantlrr 719 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) ∧ 𝑎𝑋) → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ)
126 dvmptfsum.b . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝐼𝑥𝑋) → 𝐵 ∈ ℂ)
1271263expb 1120 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖𝐼𝑥𝑋)) → 𝐵 ∈ ℂ)
128127ancom2s 648 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑖𝐼)) → 𝐵 ∈ ℂ)
129128ralrimivva 3197 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝑋𝑖𝐼 𝐵 ∈ ℂ)
13097nfel1 2923 . . . . . . . . . . . . . . . . 17 𝑥𝑎 / 𝑥𝐵 ∈ ℂ
131 nfcsb1v 3880 . . . . . . . . . . . . . . . . . 18 𝑖𝑐 / 𝑖𝑎 / 𝑥𝐵
132131nfel1 2923 . . . . . . . . . . . . . . . . 17 𝑖𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ
13399eleq1d 2822 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝐵 ∈ ℂ ↔ 𝑎 / 𝑥𝐵 ∈ ℂ))
134 csbeq1a 3869 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑐𝑎 / 𝑥𝐵 = 𝑐 / 𝑖𝑎 / 𝑥𝐵)
135134eleq1d 2822 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑎 / 𝑥𝐵 ∈ ℂ ↔ 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ))
136130, 132, 133, 135rspc2 3588 . . . . . . . . . . . . . . . 16 ((𝑎𝑋𝑐𝐼) → (∀𝑥𝑋𝑖𝐼 𝐵 ∈ ℂ → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ))
137136ancoms 459 . . . . . . . . . . . . . . 15 ((𝑐𝐼𝑎𝑋) → (∀𝑥𝑋𝑖𝐼 𝐵 ∈ ℂ → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ))
138129, 137mpan9 507 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝐼𝑎𝑋)) → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ)
139105, 112, 113, 138syl12anc 835 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ)
140139adantlrr 719 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) ∧ 𝑎𝑋) → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ)
141111ad2antrl 726 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → 𝑐𝐼)
142 nfv 1917 . . . . . . . . . . . . . . . 16 𝑖(𝜑𝑐𝐼)
143 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑖𝑆
144 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑖 D
145 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑖𝑋
146 nfcsb1v 3880 . . . . . . . . . . . . . . . . . . 19 𝑖𝑐 / 𝑖𝐴
147145, 146nfmpt 5212 . . . . . . . . . . . . . . . . . 18 𝑖(𝑥𝑋𝑐 / 𝑖𝐴)
148143, 144, 147nfov 7387 . . . . . . . . . . . . . . . . 17 𝑖(𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴))
149 nfcsb1v 3880 . . . . . . . . . . . . . . . . . 18 𝑖𝑐 / 𝑖𝐵
150145, 149nfmpt 5212 . . . . . . . . . . . . . . . . 17 𝑖(𝑥𝑋𝑐 / 𝑖𝐵)
151148, 150nfeq 2920 . . . . . . . . . . . . . . . 16 𝑖(𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵)
152142, 151nfim 1899 . . . . . . . . . . . . . . 15 𝑖((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵))
153 eleq1w 2820 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑖𝐼𝑐𝐼))
154153anbi2d 629 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑐 → ((𝜑𝑖𝐼) ↔ (𝜑𝑐𝐼)))
155 csbeq1a 3869 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑐𝐴 = 𝑐 / 𝑖𝐴)
156155mpteq2dv 5207 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑐 → (𝑥𝑋𝐴) = (𝑥𝑋𝑐 / 𝑖𝐴))
157156oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑆 D (𝑥𝑋𝐴)) = (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)))
158 csbeq1a 3869 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑐𝐵 = 𝑐 / 𝑖𝐵)
159158mpteq2dv 5207 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑥𝑋𝐵) = (𝑥𝑋𝑐 / 𝑖𝐵))
160157, 159eqeq12d 2752 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑐 → ((𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵) ↔ (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵)))
161154, 160imbi12d 344 . . . . . . . . . . . . . . 15 (𝑖 = 𝑐 → (((𝜑𝑖𝐼) → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵)) ↔ ((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵))))
162 dvmptfsum.d . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐼) → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵))
163152, 161, 162chvarfv 2233 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵))
164 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑎𝑐 / 𝑖𝐴
165 nfcv 2907 . . . . . . . . . . . . . . . . 17 𝑥𝑐
166165, 75nfcsbw 3882 . . . . . . . . . . . . . . . 16 𝑥𝑐 / 𝑖𝑎 / 𝑥𝐴
16780csbeq2dv 3862 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎𝑐 / 𝑖𝐴 = 𝑐 / 𝑖𝑎 / 𝑥𝐴)
168164, 166, 167cbvmpt 5216 . . . . . . . . . . . . . . 15 (𝑥𝑋𝑐 / 𝑖𝐴) = (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐴)
169168oveq2i 7368 . . . . . . . . . . . . . 14 (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑆 D (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐴))
170 nfcv 2907 . . . . . . . . . . . . . . 15 𝑎𝑐 / 𝑖𝐵
171165, 97nfcsbw 3882 . . . . . . . . . . . . . . 15 𝑥𝑐 / 𝑖𝑎 / 𝑥𝐵
17299csbeq2dv 3862 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎𝑐 / 𝑖𝐵 = 𝑐 / 𝑖𝑎 / 𝑥𝐵)
173170, 171, 172cbvmpt 5216 . . . . . . . . . . . . . 14 (𝑥𝑋𝑐 / 𝑖𝐵) = (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐵)
174163, 169, 1733eqtr3g 2799 . . . . . . . . . . . . 13 ((𝜑𝑐𝐼) → (𝑆 D (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐴)) = (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐵))
17566, 141, 174syl2anc 584 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐴)) = (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐵))
17667, 87, 89, 104, 125, 140, 175dvmptadd 25324 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴))) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵)))
177 nfcv 2907 . . . . . . . . . . . . . . 15 𝑎Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴
178 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑥(𝑏 ∪ {𝑐})
179178, 75nfsum 15575 . . . . . . . . . . . . . . 15 𝑥Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴
18080sumeq2sdv 15589 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴)
181177, 179, 180cbvmpt 5216 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴)
182 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → ¬ 𝑐𝑏)
183 disjsn 4672 . . . . . . . . . . . . . . . . . 18 ((𝑏 ∩ {𝑐}) = ∅ ↔ ¬ 𝑐𝑏)
184182, 183sylibr 233 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (𝑏 ∩ {𝑐}) = ∅)
185 eqidd 2737 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (𝑏 ∪ {𝑐}) = (𝑏 ∪ {𝑐}))
186 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (𝑏 ∪ {𝑐}) ⊆ 𝐼)
18768, 186ssfid 9211 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (𝑏 ∪ {𝑐}) ∈ Fin)
188 simp-4l 781 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝜑)
189186sselda 3944 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑖𝐼)
190 simplr 767 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑎𝑋)
191188, 189, 190, 84syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑎 / 𝑥𝐴 ∈ ℂ)
192184, 185, 187, 191fsumsplit 15626 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴 = (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐴))
193 sumsns 15635 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ V ∧ 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ) → Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐴 = 𝑐 / 𝑖𝑎 / 𝑥𝐴)
194109, 124, 193sylancr 587 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐴 = 𝑐 / 𝑖𝑎 / 𝑥𝐴)
195194oveq2d 7373 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐴) = (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴))
196192, 195eqtrd 2776 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴 = (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴))
197196mpteq2dva 5205 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑎𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴)))
198181, 197eqtrid 2788 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴)))
199198adantrr 715 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴)))
200199oveq2d 7373 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑆 D (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴))))
201 nfcv 2907 . . . . . . . . . . . . . 14 𝑎Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵
202178, 97nfsum 15575 . . . . . . . . . . . . . 14 𝑥Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵
20399sumeq2sdv 15589 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵)
204201, 202, 203cbvmpt 5216 . . . . . . . . . . . . 13 (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵)
20574, 130nfim 1899 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐵 ∈ ℂ)
20679, 133imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (((𝜑𝑖𝐼𝑥𝑋) → 𝐵 ∈ ℂ) ↔ ((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐵 ∈ ℂ)))
207205, 206, 126chvarfv 2233 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐵 ∈ ℂ)
208188, 189, 190, 207syl3anc 1371 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑎 / 𝑥𝐵 ∈ ℂ)
209184, 185, 187, 208fsumsplit 15626 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵 = (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐵))
210 sumsns 15635 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ V ∧ 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ) → Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐵 = 𝑐 / 𝑖𝑎 / 𝑥𝐵)
211109, 139, 210sylancr 587 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐵 = 𝑐 / 𝑖𝑎 / 𝑥𝐵)
212211oveq2d 7373 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐵) = (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵))
213209, 212eqtrd 2776 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵 = (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵))
214213mpteq2dva 5205 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑎𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵)))
215204, 214eqtrid 2788 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵)))
216215adantrr 715 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵)))
217176, 200, 2163eqtr4d 2786 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))
218217exp32 421 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑐𝑏) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵) → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
219218a2d 29 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑐𝑏) → (((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
22065, 219syl5 34 . . . . . . 7 ((𝜑 ∧ ¬ 𝑐𝑏) → ((𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
221220expcom 414 . . . . . 6 𝑐𝑏 → (𝜑 → ((𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
222221adantl 482 . . . . 5 ((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) → (𝜑 → ((𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
223222a2d 29 . . . 4 ((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) → ((𝜑 → (𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝜑 → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
22411, 20, 29, 38, 61, 223findcard2s 9109 . . 3 (𝐼 ∈ Fin → (𝜑 → (𝐼𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵))))
2252, 224mpcom 38 . 2 (𝜑 → (𝐼𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵)))
2261, 225mpi 20 1 (𝜑 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  Vcvv 3445  csb 3855  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586  {cpr 4588  cmpt 5188  cfv 6496  (class class class)co 7357  Fincfn 8883  cc 11049  cr 11050  0cc0 11051   + caddc 11054  Σcsu 15570  t crest 17302  TopOpenctopn 17303  fldccnfld 20796  TopOnctopon 22259   D cdv 25227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-icc 13271  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231
This theorem is referenced by:  dvply1  25644  dvtaylp  25729  pserdvlem2  25787  advlogexp  26010  dvnmul  44174  dirkeritg  44333  etransclem2  44467
  Copyright terms: Public domain W3C validator