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

Theorem dvmptfsum 25995
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 4001 . 2 𝐼𝐼
2 dvmptfsum.i . . 3 (𝜑𝐼 ∈ Fin)
3 sseq1 4004 . . . . . 6 (𝑎 = ∅ → (𝑎𝐼 ↔ ∅ ⊆ 𝐼))
4 sumeq1 15688 . . . . . . . . 9 (𝑎 = ∅ → Σ𝑖𝑎 𝐴 = Σ𝑖 ∈ ∅ 𝐴)
54mpteq2dv 5247 . . . . . . . 8 (𝑎 = ∅ → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴))
65oveq2d 7432 . . . . . . 7 (𝑎 = ∅ → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)))
7 sumeq1 15688 . . . . . . . 8 (𝑎 = ∅ → Σ𝑖𝑎 𝐵 = Σ𝑖 ∈ ∅ 𝐵)
87mpteq2dv 5247 . . . . . . 7 (𝑎 = ∅ → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))
96, 8eqeq12d 2742 . . . . . 6 (𝑎 = ∅ → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) ↔ (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))
103, 9imbi12d 343 . . . . 5 (𝑎 = ∅ → ((𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵)) ↔ (∅ ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))))
1110imbi2d 339 . . . 4 (𝑎 = ∅ → ((𝜑 → (𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵))) ↔ (𝜑 → (∅ ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))))
12 sseq1 4004 . . . . . 6 (𝑎 = 𝑏 → (𝑎𝐼𝑏𝐼))
13 sumeq1 15688 . . . . . . . . 9 (𝑎 = 𝑏 → Σ𝑖𝑎 𝐴 = Σ𝑖𝑏 𝐴)
1413mpteq2dv 5247 . . . . . . . 8 (𝑎 = 𝑏 → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴))
1514oveq2d 7432 . . . . . . 7 (𝑎 = 𝑏 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)))
16 sumeq1 15688 . . . . . . . 8 (𝑎 = 𝑏 → Σ𝑖𝑎 𝐵 = Σ𝑖𝑏 𝐵)
1716mpteq2dv 5247 . . . . . . 7 (𝑎 = 𝑏 → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))
1815, 17eqeq12d 2742 . . . . . 6 (𝑎 = 𝑏 → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) ↔ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)))
1912, 18imbi12d 343 . . . . 5 (𝑎 = 𝑏 → ((𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵)) ↔ (𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))))
2019imbi2d 339 . . . 4 (𝑎 = 𝑏 → ((𝜑 → (𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵))) ↔ (𝜑 → (𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)))))
21 sseq1 4004 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎𝐼 ↔ (𝑏 ∪ {𝑐}) ⊆ 𝐼))
22 sumeq1 15688 . . . . . . . . 9 (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑖𝑎 𝐴 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)
2322mpteq2dv 5247 . . . . . . . 8 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴))
2423oveq2d 7432 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)))
25 sumeq1 15688 . . . . . . . 8 (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑖𝑎 𝐵 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)
2625mpteq2dv 5247 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))
2724, 26eqeq12d 2742 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) ↔ (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))
2821, 27imbi12d 343 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵)) ↔ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
2928imbi2d 339 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝜑 → (𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵))) ↔ (𝜑 → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
30 sseq1 4004 . . . . . 6 (𝑎 = 𝐼 → (𝑎𝐼𝐼𝐼))
31 sumeq1 15688 . . . . . . . . 9 (𝑎 = 𝐼 → Σ𝑖𝑎 𝐴 = Σ𝑖𝐼 𝐴)
3231mpteq2dv 5247 . . . . . . . 8 (𝑎 = 𝐼 → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴))
3332oveq2d 7432 . . . . . . 7 (𝑎 = 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)))
34 sumeq1 15688 . . . . . . . 8 (𝑎 = 𝐼 → Σ𝑖𝑎 𝐵 = Σ𝑖𝐼 𝐵)
3534mpteq2dv 5247 . . . . . . 7 (𝑎 = 𝐼 → (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵))
3633, 35eqeq12d 2742 . . . . . 6 (𝑎 = 𝐼 → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵) ↔ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵)))
3730, 36imbi12d 343 . . . . 5 (𝑎 = 𝐼 → ((𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵)) ↔ (𝐼𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵))))
3837imbi2d 339 . . . 4 (𝑎 = 𝐼 → ((𝜑 → (𝑎𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑎 𝐵))) ↔ (𝜑 → (𝐼𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝐼 𝐵)))))
39 dvmptfsum.s . . . . . . 7 (𝜑𝑆 ∈ {ℝ, ℂ})
40 0cnd 11248 . . . . . . 7 ((𝜑𝑥𝑆) → 0 ∈ ℂ)
41 0cnd 11248 . . . . . . . 8 (𝜑 → 0 ∈ ℂ)
4239, 41dvmptc 25978 . . . . . . 7 (𝜑 → (𝑆 D (𝑥𝑆 ↦ 0)) = (𝑥𝑆 ↦ 0))
43 dvmptfsum.j . . . . . . . . 9 𝐽 = (𝐾t 𝑆)
44 dvmptfsum.k . . . . . . . . . . 11 𝐾 = (TopOpen‘ℂfld)
4544cnfldtopon 24787 . . . . . . . . . 10 𝐾 ∈ (TopOn‘ℂ)
46 recnprss 25921 . . . . . . . . . . 11 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
4739, 46syl 17 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℂ)
48 resttopon 23153 . . . . . . . . . 10 ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾t 𝑆) ∈ (TopOn‘𝑆))
4945, 47, 48sylancr 585 . . . . . . . . 9 (𝜑 → (𝐾t 𝑆) ∈ (TopOn‘𝑆))
5043, 49eqeltrid 2830 . . . . . . . 8 (𝜑𝐽 ∈ (TopOn‘𝑆))
51 dvmptfsum.x . . . . . . . 8 (𝜑𝑋𝐽)
52 toponss 22917 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑆) ∧ 𝑋𝐽) → 𝑋𝑆)
5350, 51, 52syl2anc 582 . . . . . . 7 (𝜑𝑋𝑆)
5439, 40, 40, 42, 53, 43, 44, 51dvmptres 25983 . . . . . 6 (𝜑 → (𝑆 D (𝑥𝑋 ↦ 0)) = (𝑥𝑋 ↦ 0))
55 sum0 15720 . . . . . . . 8 Σ𝑖 ∈ ∅ 𝐴 = 0
5655mpteq2i 5250 . . . . . . 7 (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴) = (𝑥𝑋 ↦ 0)
5756oveq2i 7427 . . . . . 6 (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑆 D (𝑥𝑋 ↦ 0))
58 sum0 15720 . . . . . . 7 Σ𝑖 ∈ ∅ 𝐵 = 0
5958mpteq2i 5250 . . . . . 6 (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵) = (𝑥𝑋 ↦ 0)
6054, 57, 593eqtr4g 2791 . . . . 5 (𝜑 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵))
6160a1d 25 . . . 4 (𝜑 → (∅ ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ ∅ 𝐵)))
62 ssun1 4170 . . . . . . . . . 10 𝑏 ⊆ (𝑏 ∪ {𝑐})
63 sstr 3987 . . . . . . . . . 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 9294 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑏 ∈ Fin)
71 simp-4l 781 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖𝑏) → 𝜑)
7269sselda 3978 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖𝑏) → 𝑖𝐼)
73 simplr 767 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖𝑏) → 𝑎𝑋)
74 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑥(𝜑𝑖𝐼𝑎𝑋)
75 nfcsb1v 3916 . . . . . . . . . . . . . . . . . 18 𝑥𝑎 / 𝑥𝐴
7675nfel1 2909 . . . . . . . . . . . . . . . . 17 𝑥𝑎 / 𝑥𝐴 ∈ ℂ
7774, 76nfim 1892 . . . . . . . . . . . . . . . 16 𝑥((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐴 ∈ ℂ)
78 eleq1w 2809 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (𝑥𝑋𝑎𝑋))
79783anbi3d 1439 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → ((𝜑𝑖𝐼𝑥𝑋) ↔ (𝜑𝑖𝐼𝑎𝑋)))
80 csbeq1a 3905 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎𝐴 = 𝑎 / 𝑥𝐴)
8180eleq1d 2811 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝐴 ∈ ℂ ↔ 𝑎 / 𝑥𝐴 ∈ ℂ))
8279, 81imbi12d 343 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (((𝜑𝑖𝐼𝑥𝑋) → 𝐴 ∈ ℂ) ↔ ((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐴 ∈ ℂ)))
83 dvmptfsum.a . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝐼𝑥𝑋) → 𝐴 ∈ ℂ)
8477, 82, 83chvarfv 2229 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐴 ∈ ℂ)
8571, 72, 73, 84syl3anc 1368 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖𝑏) → 𝑎 / 𝑥𝐴 ∈ ℂ)
8670, 85fsumcl 15732 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖𝑏 𝑎 / 𝑥𝐴 ∈ ℂ)
8786adantlrr 719 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) ∧ 𝑎𝑋) → Σ𝑖𝑏 𝑎 / 𝑥𝐴 ∈ ℂ)
88 sumex 15687 . . . . . . . . . . . . 13 Σ𝑖𝑏 𝑎 / 𝑥𝐵 ∈ V
8988a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) ∧ 𝑎𝑋) → Σ𝑖𝑏 𝑎 / 𝑥𝐵 ∈ V)
90 nfcv 2892 . . . . . . . . . . . . . . . . 17 𝑎Σ𝑖𝑏 𝐴
91 nfcv 2892 . . . . . . . . . . . . . . . . . 18 𝑥𝑏
9291, 75nfsum 15690 . . . . . . . . . . . . . . . . 17 𝑥Σ𝑖𝑏 𝑎 / 𝑥𝐴
9380sumeq2sdv 15703 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → Σ𝑖𝑏 𝐴 = Σ𝑖𝑏 𝑎 / 𝑥𝐴)
9490, 92, 93cbvmpt 5256 . . . . . . . . . . . . . . . 16 (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴)
9594oveq2i 7427 . . . . . . . . . . . . . . 15 (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑆 D (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴))
96 nfcv 2892 . . . . . . . . . . . . . . . 16 𝑎Σ𝑖𝑏 𝐵
97 nfcsb1v 3916 . . . . . . . . . . . . . . . . 17 𝑥𝑎 / 𝑥𝐵
9891, 97nfsum 15690 . . . . . . . . . . . . . . . 16 𝑥Σ𝑖𝑏 𝑎 / 𝑥𝐵
99 csbeq1a 3905 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎𝐵 = 𝑎 / 𝑥𝐵)
10099sumeq2sdv 15703 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → Σ𝑖𝑏 𝐵 = Σ𝑖𝑏 𝑎 / 𝑥𝐵)
10196, 98, 100cbvmpt 5256 . . . . . . . . . . . . . . 15 (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐵)
10295, 101eqeq12i 2744 . . . . . . . . . . . . . 14 ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵) ↔ (𝑆 D (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴)) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐵))
103102biimpi 215 . . . . . . . . . . . . 13 ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵) → (𝑆 D (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴)) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐵))
104103ad2antll 727 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐴)) = (𝑎𝑋 ↦ Σ𝑖𝑏 𝑎 / 𝑥𝐵))
105 simplll 773 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝜑)
106 ssun2 4171 . . . . . . . . . . . . . . . . 17 {𝑐} ⊆ (𝑏 ∪ {𝑐})
107 sstr 3987 . . . . . . . . . . . . . . . . 17 (({𝑐} ⊆ (𝑏 ∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → {𝑐} ⊆ 𝐼)
108106, 107mpan 688 . . . . . . . . . . . . . . . 16 ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → {𝑐} ⊆ 𝐼)
109 vex 3466 . . . . . . . . . . . . . . . . 17 𝑐 ∈ V
110109snss 4784 . . . . . . . . . . . . . . . 16 (𝑐𝐼 ↔ {𝑐} ⊆ 𝐼)
111108, 110sylibr 233 . . . . . . . . . . . . . . 15 ((𝑏 ∪ {𝑐}) ⊆ 𝐼𝑐𝐼)
112111ad2antlr 725 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑐𝐼)
113 simpr 483 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑎𝑋)
114833expb 1117 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖𝐼𝑥𝑋)) → 𝐴 ∈ ℂ)
115114ancom2s 648 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑖𝐼)) → 𝐴 ∈ ℂ)
116115ralrimivva 3191 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝑋𝑖𝐼 𝐴 ∈ ℂ)
117 nfcsb1v 3916 . . . . . . . . . . . . . . . . . 18 𝑖𝑐 / 𝑖𝑎 / 𝑥𝐴
118117nfel1 2909 . . . . . . . . . . . . . . . . 17 𝑖𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ
119 csbeq1a 3905 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑐𝑎 / 𝑥𝐴 = 𝑐 / 𝑖𝑎 / 𝑥𝐴)
120119eleq1d 2811 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑎 / 𝑥𝐴 ∈ ℂ ↔ 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ))
12176, 118, 81, 120rspc2 3616 . . . . . . . . . . . . . . . 16 ((𝑎𝑋𝑐𝐼) → (∀𝑥𝑋𝑖𝐼 𝐴 ∈ ℂ → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ))
122121ancoms 457 . . . . . . . . . . . . . . 15 ((𝑐𝐼𝑎𝑋) → (∀𝑥𝑋𝑖𝐼 𝐴 ∈ ℂ → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ))
123116, 122mpan9 505 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝐼𝑎𝑋)) → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ)
124105, 112, 113, 123syl12anc 835 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ)
125124adantlrr 719 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) ∧ 𝑎𝑋) → 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ)
126 dvmptfsum.b . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝐼𝑥𝑋) → 𝐵 ∈ ℂ)
1271263expb 1117 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖𝐼𝑥𝑋)) → 𝐵 ∈ ℂ)
128127ancom2s 648 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑖𝐼)) → 𝐵 ∈ ℂ)
129128ralrimivva 3191 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝑋𝑖𝐼 𝐵 ∈ ℂ)
13097nfel1 2909 . . . . . . . . . . . . . . . . 17 𝑥𝑎 / 𝑥𝐵 ∈ ℂ
131 nfcsb1v 3916 . . . . . . . . . . . . . . . . . 18 𝑖𝑐 / 𝑖𝑎 / 𝑥𝐵
132131nfel1 2909 . . . . . . . . . . . . . . . . 17 𝑖𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ
13399eleq1d 2811 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝐵 ∈ ℂ ↔ 𝑎 / 𝑥𝐵 ∈ ℂ))
134 csbeq1a 3905 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑐𝑎 / 𝑥𝐵 = 𝑐 / 𝑖𝑎 / 𝑥𝐵)
135134eleq1d 2811 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑎 / 𝑥𝐵 ∈ ℂ ↔ 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ))
136130, 132, 133, 135rspc2 3616 . . . . . . . . . . . . . . . 16 ((𝑎𝑋𝑐𝐼) → (∀𝑥𝑋𝑖𝐼 𝐵 ∈ ℂ → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ))
137136ancoms 457 . . . . . . . . . . . . . . 15 ((𝑐𝐼𝑎𝑋) → (∀𝑥𝑋𝑖𝐼 𝐵 ∈ ℂ → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ))
138129, 137mpan9 505 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝐼𝑎𝑋)) → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ)
139105, 112, 113, 138syl12anc 835 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ)
140139adantlrr 719 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) ∧ 𝑎𝑋) → 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ)
141111ad2antrl 726 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → 𝑐𝐼)
142 nfv 1910 . . . . . . . . . . . . . . . 16 𝑖(𝜑𝑐𝐼)
143 nfcv 2892 . . . . . . . . . . . . . . . . . 18 𝑖𝑆
144 nfcv 2892 . . . . . . . . . . . . . . . . . 18 𝑖 D
145 nfcv 2892 . . . . . . . . . . . . . . . . . . 19 𝑖𝑋
146 nfcsb1v 3916 . . . . . . . . . . . . . . . . . . 19 𝑖𝑐 / 𝑖𝐴
147145, 146nfmpt 5252 . . . . . . . . . . . . . . . . . 18 𝑖(𝑥𝑋𝑐 / 𝑖𝐴)
148143, 144, 147nfov 7446 . . . . . . . . . . . . . . . . 17 𝑖(𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴))
149 nfcsb1v 3916 . . . . . . . . . . . . . . . . . 18 𝑖𝑐 / 𝑖𝐵
150145, 149nfmpt 5252 . . . . . . . . . . . . . . . . 17 𝑖(𝑥𝑋𝑐 / 𝑖𝐵)
151148, 150nfeq 2906 . . . . . . . . . . . . . . . 16 𝑖(𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵)
152142, 151nfim 1892 . . . . . . . . . . . . . . 15 𝑖((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵))
153 eleq1w 2809 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑖𝐼𝑐𝐼))
154153anbi2d 628 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑐 → ((𝜑𝑖𝐼) ↔ (𝜑𝑐𝐼)))
155 csbeq1a 3905 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑐𝐴 = 𝑐 / 𝑖𝐴)
156155mpteq2dv 5247 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑐 → (𝑥𝑋𝐴) = (𝑥𝑋𝑐 / 𝑖𝐴))
157156oveq2d 7432 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑆 D (𝑥𝑋𝐴)) = (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)))
158 csbeq1a 3905 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑐𝐵 = 𝑐 / 𝑖𝐵)
159158mpteq2dv 5247 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑐 → (𝑥𝑋𝐵) = (𝑥𝑋𝑐 / 𝑖𝐵))
160157, 159eqeq12d 2742 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑐 → ((𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵) ↔ (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵)))
161154, 160imbi12d 343 . . . . . . . . . . . . . . 15 (𝑖 = 𝑐 → (((𝜑𝑖𝐼) → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵)) ↔ ((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵))))
162 dvmptfsum.d . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐼) → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵))
163152, 161, 162chvarfv 2229 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑖𝐵))
164 nfcv 2892 . . . . . . . . . . . . . . . 16 𝑎𝑐 / 𝑖𝐴
165 nfcv 2892 . . . . . . . . . . . . . . . . 17 𝑥𝑐
166165, 75nfcsbw 3918 . . . . . . . . . . . . . . . 16 𝑥𝑐 / 𝑖𝑎 / 𝑥𝐴
16780csbeq2dv 3898 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎𝑐 / 𝑖𝐴 = 𝑐 / 𝑖𝑎 / 𝑥𝐴)
168164, 166, 167cbvmpt 5256 . . . . . . . . . . . . . . 15 (𝑥𝑋𝑐 / 𝑖𝐴) = (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐴)
169168oveq2i 7427 . . . . . . . . . . . . . 14 (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑆 D (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐴))
170 nfcv 2892 . . . . . . . . . . . . . . 15 𝑎𝑐 / 𝑖𝐵
171165, 97nfcsbw 3918 . . . . . . . . . . . . . . 15 𝑥𝑐 / 𝑖𝑎 / 𝑥𝐵
17299csbeq2dv 3898 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎𝑐 / 𝑖𝐵 = 𝑐 / 𝑖𝑎 / 𝑥𝐵)
173170, 171, 172cbvmpt 5256 . . . . . . . . . . . . . 14 (𝑥𝑋𝑐 / 𝑖𝐵) = (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐵)
174163, 169, 1733eqtr3g 2789 . . . . . . . . . . . . 13 ((𝜑𝑐𝐼) → (𝑆 D (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐴)) = (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐵))
17566, 141, 174syl2anc 582 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐴)) = (𝑎𝑋𝑐 / 𝑖𝑎 / 𝑥𝐵))
17667, 87, 89, 104, 125, 140, 175dvmptadd 25980 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴))) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵)))
177 nfcv 2892 . . . . . . . . . . . . . . 15 𝑎Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴
178 nfcv 2892 . . . . . . . . . . . . . . . 16 𝑥(𝑏 ∪ {𝑐})
179178, 75nfsum 15690 . . . . . . . . . . . . . . 15 𝑥Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴
18080sumeq2sdv 15703 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴)
181177, 179, 180cbvmpt 5256 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴)
182 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → ¬ 𝑐𝑏)
183 disjsn 4710 . . . . . . . . . . . . . . . . . 18 ((𝑏 ∩ {𝑐}) = ∅ ↔ ¬ 𝑐𝑏)
184182, 183sylibr 233 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (𝑏 ∩ {𝑐}) = ∅)
185 eqidd 2727 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (𝑏 ∪ {𝑐}) = (𝑏 ∪ {𝑐}))
186 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (𝑏 ∪ {𝑐}) ⊆ 𝐼)
18768, 186ssfid 9294 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (𝑏 ∪ {𝑐}) ∈ Fin)
188 simp-4l 781 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝜑)
189186sselda 3978 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑖𝐼)
190 simplr 767 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑎𝑋)
191188, 189, 190, 84syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑎 / 𝑥𝐴 ∈ ℂ)
192184, 185, 187, 191fsumsplit 15740 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴 = (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐴))
193 sumsns 15749 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ V ∧ 𝑐 / 𝑖𝑎 / 𝑥𝐴 ∈ ℂ) → Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐴 = 𝑐 / 𝑖𝑎 / 𝑥𝐴)
194109, 124, 193sylancr 585 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐴 = 𝑐 / 𝑖𝑎 / 𝑥𝐴)
195194oveq2d 7432 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐴) = (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴))
196192, 195eqtrd 2766 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴 = (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴))
197196mpteq2dva 5245 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑎𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐴) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴)))
198181, 197eqtrid 2778 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴)))
199198adantrr 715 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴)))
200199oveq2d 7432 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑆 D (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐴 + 𝑐 / 𝑖𝑎 / 𝑥𝐴))))
201 nfcv 2892 . . . . . . . . . . . . . 14 𝑎Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵
202178, 97nfsum 15690 . . . . . . . . . . . . . 14 𝑥Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵
20399sumeq2sdv 15703 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵 = Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵)
204201, 202, 203cbvmpt 5256 . . . . . . . . . . . . 13 (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵)
20574, 130nfim 1892 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐵 ∈ ℂ)
20679, 133imbi12d 343 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (((𝜑𝑖𝐼𝑥𝑋) → 𝐵 ∈ ℂ) ↔ ((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐵 ∈ ℂ)))
207205, 206, 126chvarfv 2229 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝐼𝑎𝑋) → 𝑎 / 𝑥𝐵 ∈ ℂ)
208188, 189, 190, 207syl3anc 1368 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) ∧ 𝑖 ∈ (𝑏 ∪ {𝑐})) → 𝑎 / 𝑥𝐵 ∈ ℂ)
209184, 185, 187, 208fsumsplit 15740 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵 = (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐵))
210 sumsns 15749 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ V ∧ 𝑐 / 𝑖𝑎 / 𝑥𝐵 ∈ ℂ) → Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐵 = 𝑐 / 𝑖𝑎 / 𝑥𝐵)
211109, 139, 210sylancr 585 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐵 = 𝑐 / 𝑖𝑎 / 𝑥𝐵)
212211oveq2d 7432 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + Σ𝑖 ∈ {𝑐}𝑎 / 𝑥𝐵) = (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵))
213209, 212eqtrd 2766 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑎𝑋) → Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵 = (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵))
214213mpteq2dva 5245 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑎𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝑎 / 𝑥𝐵) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵)))
215204, 214eqtrid 2778 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵)))
216215adantrr 715 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵) = (𝑎𝑋 ↦ (Σ𝑖𝑏 𝑎 / 𝑥𝐵 + 𝑐 / 𝑖𝑎 / 𝑥𝐵)))
217176, 200, 2163eqtr4d 2776 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑐𝑏) ∧ ((𝑏 ∪ {𝑐}) ⊆ 𝐼 ∧ (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))
218217exp32 419 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑐𝑏) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → ((𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵) → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
219218a2d 29 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑐𝑏) → (((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
22065, 219syl5 34 . . . . . . 7 ((𝜑 ∧ ¬ 𝑐𝑏) → ((𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵))))
221220expcom 412 . . . . . 6 𝑐𝑏 → (𝜑 → ((𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
222221adantl 480 . . . . 5 ((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) → (𝜑 → ((𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵)) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
223222a2d 29 . . . 4 ((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) → ((𝜑 → (𝑏𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑖𝑏 𝐵))) → (𝜑 → ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑆 D (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑖 ∈ (𝑏 ∪ {𝑐})𝐵)))))
22411, 20, 29, 38, 61, 223findcard2s 9195 . . 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 394  w3a 1084   = wceq 1534  wcel 2099  wral 3051  Vcvv 3462  csb 3891  cun 3944  cin 3945  wss 3946  c0 4322  {csn 4623  {cpr 4625  cmpt 5228  cfv 6546  (class class class)co 7416  Fincfn 8966  cc 11147  cr 11148  0cc0 11149   + caddc 11152  Σcsu 15685  t crest 17430  TopOpenctopn 17431  fldccnfld 21339  TopOnctopon 22900   D cdv 25880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-inf2 9677  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227  ax-addf 11228
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-om 7869  df-1st 7995  df-2nd 7996  df-supp 8167  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-er 8726  df-map 8849  df-pm 8850  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9399  df-fi 9447  df-sup 9478  df-inf 9479  df-oi 9546  df-card 9975  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12519  df-z 12605  df-dec 12724  df-uz 12869  df-q 12979  df-rp 13023  df-xneg 13140  df-xadd 13141  df-xmul 13142  df-icc 13379  df-fz 13533  df-fzo 13676  df-seq 14016  df-exp 14076  df-hash 14343  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-clim 15485  df-sum 15686  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-starv 17276  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-hom 17285  df-cco 17286  df-rest 17432  df-topn 17433  df-0g 17451  df-gsum 17452  df-topgen 17453  df-pt 17454  df-prds 17457  df-xrs 17512  df-qtop 17517  df-imas 17518  df-xps 17520  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-submnd 18769  df-mulg 19058  df-cntz 19307  df-cmn 19776  df-psmet 21331  df-xmet 21332  df-met 21333  df-bl 21334  df-mopn 21335  df-fbas 21336  df-fg 21337  df-cnfld 21340  df-top 22884  df-topon 22901  df-topsp 22923  df-bases 22937  df-cld 23011  df-ntr 23012  df-cls 23013  df-nei 23090  df-lp 23128  df-perf 23129  df-cn 23219  df-cnp 23220  df-haus 23307  df-tx 23554  df-hmeo 23747  df-fil 23838  df-fm 23930  df-flim 23931  df-flf 23932  df-xms 24314  df-ms 24315  df-tms 24316  df-cncf 24886  df-limc 25883  df-dv 25884
This theorem is referenced by:  dvply1  26308  dvtaylp  26395  pserdvlem2  26455  advlogexp  26679  dvnmul  45600  dirkeritg  45759  etransclem2  45893
  Copyright terms: Public domain W3C validator