Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvmptfprod Structured version   Visualization version   GIF version

Theorem dvmptfprod 45901
Description: Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvmptfprod.iph 𝑖𝜑
dvmptfprod.jph 𝑗𝜑
dvmptfprod.j 𝐽 = (𝐾t 𝑆)
dvmptfprod.k 𝐾 = (TopOpen‘ℂfld)
dvmptfprod.s (𝜑𝑆 ∈ {ℝ, ℂ})
dvmptfprod.x (𝜑𝑋𝐽)
dvmptfprod.i (𝜑𝐼 ∈ Fin)
dvmptfprod.a ((𝜑𝑖𝐼𝑥𝑋) → 𝐴 ∈ ℂ)
dvmptfprod.b ((𝜑𝑖𝐼𝑥𝑋) → 𝐵 ∈ ℂ)
dvmptfprod.d ((𝜑𝑖𝐼) → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵))
dvmptfprod.bc (𝑖 = 𝑗𝐵 = 𝐶)
Assertion
Ref Expression
dvmptfprod (𝜑 → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴)))
Distinct variable groups:   𝐴,𝑗   𝐶,𝑖   𝑖,𝐼,𝑗,𝑥   𝑆,𝑖,𝑗,𝑥   𝑖,𝑋,𝑗,𝑥   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑖,𝑗)   𝐴(𝑥,𝑖)   𝐵(𝑥,𝑖,𝑗)   𝐶(𝑥,𝑗)   𝐽(𝑥,𝑖,𝑗)   𝐾(𝑥,𝑖,𝑗)

Proof of Theorem dvmptfprod
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvmptfprod.i . 2 (𝜑𝐼 ∈ Fin)
2 ssid 4018 . . 3 𝐼𝐼
32jctr 524 . 2 (𝜑 → (𝜑𝐼𝐼))
4 sseq1 4021 . . . . 5 (𝑎 = ∅ → (𝑎𝐼 ↔ ∅ ⊆ 𝐼))
54anbi2d 630 . . . 4 (𝑎 = ∅ → ((𝜑𝑎𝐼) ↔ (𝜑 ∧ ∅ ⊆ 𝐼)))
6 prodeq1 15940 . . . . . . 7 (𝑎 = ∅ → ∏𝑖𝑎 𝐴 = ∏𝑖 ∈ ∅ 𝐴)
76mpteq2dv 5250 . . . . . 6 (𝑎 = ∅ → (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴) = (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴))
87oveq2d 7447 . . . . 5 (𝑎 = ∅ → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴)))
9 sumeq1 15722 . . . . . . 7 (𝑎 = ∅ → Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴))
10 difeq1 4129 . . . . . . . . . 10 (𝑎 = ∅ → (𝑎 ∖ {𝑗}) = (∅ ∖ {𝑗}))
1110prodeq1d 15953 . . . . . . . . 9 (𝑎 = ∅ → ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴 = ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴)
1211oveq2d 7447 . . . . . . . 8 (𝑎 = ∅ → (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴))
1312sumeq2sdv 15736 . . . . . . 7 (𝑎 = ∅ → Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴))
149, 13eqtrd 2775 . . . . . 6 (𝑎 = ∅ → Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴))
1514mpteq2dv 5250 . . . . 5 (𝑎 = ∅ → (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴)))
168, 15eqeq12d 2751 . . . 4 (𝑎 = ∅ → ((𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴)) ↔ (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴))))
175, 16imbi12d 344 . . 3 (𝑎 = ∅ → (((𝜑𝑎𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴))) ↔ ((𝜑 ∧ ∅ ⊆ 𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴)))))
18 sseq1 4021 . . . . 5 (𝑎 = 𝑏 → (𝑎𝐼𝑏𝐼))
1918anbi2d 630 . . . 4 (𝑎 = 𝑏 → ((𝜑𝑎𝐼) ↔ (𝜑𝑏𝐼)))
20 prodeq1 15940 . . . . . . 7 (𝑎 = 𝑏 → ∏𝑖𝑎 𝐴 = ∏𝑖𝑏 𝐴)
2120mpteq2dv 5250 . . . . . 6 (𝑎 = 𝑏 → (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴) = (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴))
2221oveq2d 7447 . . . . 5 (𝑎 = 𝑏 → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)))
23 sumeq1 15722 . . . . . . 7 (𝑎 = 𝑏 → Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴))
24 difeq1 4129 . . . . . . . . . 10 (𝑎 = 𝑏 → (𝑎 ∖ {𝑗}) = (𝑏 ∖ {𝑗}))
2524prodeq1d 15953 . . . . . . . . 9 (𝑎 = 𝑏 → ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴 = ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)
2625oveq2d 7447 . . . . . . . 8 (𝑎 = 𝑏 → (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
2726sumeq2sdv 15736 . . . . . . 7 (𝑎 = 𝑏 → Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
2823, 27eqtrd 2775 . . . . . 6 (𝑎 = 𝑏 → Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
2928mpteq2dv 5250 . . . . 5 (𝑎 = 𝑏 → (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)))
3022, 29eqeq12d 2751 . . . 4 (𝑎 = 𝑏 → ((𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴)) ↔ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))))
3119, 30imbi12d 344 . . 3 (𝑎 = 𝑏 → (((𝜑𝑎𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴))) ↔ ((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)))))
32 sseq1 4021 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎𝐼 ↔ (𝑏 ∪ {𝑐}) ⊆ 𝐼))
3332anbi2d 630 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝜑𝑎𝐼) ↔ (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)))
34 prodeq1 15940 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → ∏𝑖𝑎 𝐴 = ∏𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)
3534mpteq2dv 5250 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴) = (𝑥𝑋 ↦ ∏𝑖 ∈ (𝑏 ∪ {𝑐})𝐴))
3635oveq2d 7447 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)))
37 sumeq1 15722 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴))
38 difeq1 4129 . . . . . . . . . 10 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ∖ {𝑗}) = ((𝑏 ∪ {𝑐}) ∖ {𝑗}))
3938prodeq1d 15953 . . . . . . . . 9 (𝑎 = (𝑏 ∪ {𝑐}) → ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴 = ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴)
4039oveq2d 7447 . . . . . . . 8 (𝑎 = (𝑏 ∪ {𝑐}) → (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = (𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴))
4140sumeq2sdv 15736 . . . . . . 7 (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴))
4237, 41eqtrd 2775 . . . . . 6 (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴))
4342mpteq2dv 5250 . . . . 5 (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴)))
4436, 43eqeq12d 2751 . . . 4 (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴)) ↔ (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴))))
4533, 44imbi12d 344 . . 3 (𝑎 = (𝑏 ∪ {𝑐}) → (((𝜑𝑎𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴))) ↔ ((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴)))))
46 sseq1 4021 . . . . 5 (𝑎 = 𝐼 → (𝑎𝐼𝐼𝐼))
4746anbi2d 630 . . . 4 (𝑎 = 𝐼 → ((𝜑𝑎𝐼) ↔ (𝜑𝐼𝐼)))
48 prodeq1 15940 . . . . . . 7 (𝑎 = 𝐼 → ∏𝑖𝑎 𝐴 = ∏𝑖𝐼 𝐴)
4948mpteq2dv 5250 . . . . . 6 (𝑎 = 𝐼 → (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴) = (𝑥𝑋 ↦ ∏𝑖𝐼 𝐴))
5049oveq2d 7447 . . . . 5 (𝑎 = 𝐼 → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝐼 𝐴)))
51 sumeq1 15722 . . . . . . 7 (𝑎 = 𝐼 → Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴))
52 difeq1 4129 . . . . . . . . . 10 (𝑎 = 𝐼 → (𝑎 ∖ {𝑗}) = (𝐼 ∖ {𝑗}))
5352prodeq1d 15953 . . . . . . . . 9 (𝑎 = 𝐼 → ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴 = ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴)
5453oveq2d 7447 . . . . . . . 8 (𝑎 = 𝐼 → (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴))
5554sumeq2sdv 15736 . . . . . . 7 (𝑎 = 𝐼 → Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴))
5651, 55eqtrd 2775 . . . . . 6 (𝑎 = 𝐼 → Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴) = Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴))
5756mpteq2dv 5250 . . . . 5 (𝑎 = 𝐼 → (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴)))
5850, 57eqeq12d 2751 . . . 4 (𝑎 = 𝐼 → ((𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴)) ↔ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴))))
5947, 58imbi12d 344 . . 3 (𝑎 = 𝐼 → (((𝜑𝑎𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑎 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑎 (𝐶 · ∏𝑖 ∈ (𝑎 ∖ {𝑗})𝐴))) ↔ ((𝜑𝐼𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴)))))
60 prod0 15976 . . . . . . . 8 𝑖 ∈ ∅ 𝐴 = 1
6160mpteq2i 5253 . . . . . . 7 (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴) = (𝑥𝑋 ↦ 1)
6261oveq2i 7442 . . . . . 6 (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴)) = (𝑆 D (𝑥𝑋 ↦ 1))
6362a1i 11 . . . . 5 (𝜑 → (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴)) = (𝑆 D (𝑥𝑋 ↦ 1)))
64 dvmptfprod.s . . . . . 6 (𝜑𝑆 ∈ {ℝ, ℂ})
65 dvmptfprod.x . . . . . . 7 (𝜑𝑋𝐽)
66 dvmptfprod.j . . . . . . . 8 𝐽 = (𝐾t 𝑆)
67 dvmptfprod.k . . . . . . . . 9 𝐾 = (TopOpen‘ℂfld)
6867oveq1i 7441 . . . . . . . 8 (𝐾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
6966, 68eqtri 2763 . . . . . . 7 𝐽 = ((TopOpen‘ℂfld) ↾t 𝑆)
7065, 69eleqtrdi 2849 . . . . . 6 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
71 1cnd 11254 . . . . . 6 (𝜑 → 1 ∈ ℂ)
7264, 70, 71dvmptconst 45871 . . . . 5 (𝜑 → (𝑆 D (𝑥𝑋 ↦ 1)) = (𝑥𝑋 ↦ 0))
73 sum0 15754 . . . . . . . 8 Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴) = 0
7473eqcomi 2744 . . . . . . 7 0 = Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴)
7574mpteq2i 5253 . . . . . 6 (𝑥𝑋 ↦ 0) = (𝑥𝑋 ↦ Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴))
7675a1i 11 . . . . 5 (𝜑 → (𝑥𝑋 ↦ 0) = (𝑥𝑋 ↦ Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴)))
7763, 72, 763eqtrd 2779 . . . 4 (𝜑 → (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴)))
7877adantr 480 . . 3 ((𝜑 ∧ ∅ ⊆ 𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ ∅ 𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ ∅ (𝐶 · ∏𝑖 ∈ (∅ ∖ {𝑗})𝐴)))
79 simp3 1137 . . . . 5 (((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) ∧ ((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)) → (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼))
80 simp1r 1197 . . . . 5 (((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) ∧ ((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)) → ¬ 𝑐𝑏)
81 ssun1 4188 . . . . . . . . . 10 𝑏 ⊆ (𝑏 ∪ {𝑐})
82 sstr2 4002 . . . . . . . . . 10 (𝑏 ⊆ (𝑏 ∪ {𝑐}) → ((𝑏 ∪ {𝑐}) ⊆ 𝐼𝑏𝐼))
8381, 82ax-mp 5 . . . . . . . . 9 ((𝑏 ∪ {𝑐}) ⊆ 𝐼𝑏𝐼)
8483anim2i 617 . . . . . . . 8 ((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝜑𝑏𝐼))
8584adantl 481 . . . . . . 7 ((((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)) → (𝜑𝑏𝐼))
86 simpl 482 . . . . . . 7 ((((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)) → ((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))))
8785, 86mpd 15 . . . . . 6 ((((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)))
88873adant1 1129 . . . . 5 (((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) ∧ ((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)))
89 nfv 1912 . . . . . . 7 𝑥((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏)
90 nfcv 2903 . . . . . . . . 9 𝑥𝑆
91 nfcv 2903 . . . . . . . . 9 𝑥 D
92 nfmpt1 5256 . . . . . . . . 9 𝑥(𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)
9390, 91, 92nfov 7461 . . . . . . . 8 𝑥(𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴))
94 nfmpt1 5256 . . . . . . . 8 𝑥(𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
9593, 94nfeq 2917 . . . . . . 7 𝑥(𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
9689, 95nfan 1897 . . . . . 6 𝑥(((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)))
97 dvmptfprod.iph . . . . . . . . 9 𝑖𝜑
98 nfv 1912 . . . . . . . . 9 𝑖(𝑏 ∪ {𝑐}) ⊆ 𝐼
9997, 98nfan 1897 . . . . . . . 8 𝑖(𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)
100 nfv 1912 . . . . . . . 8 𝑖 ¬ 𝑐𝑏
10199, 100nfan 1897 . . . . . . 7 𝑖((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏)
102 nfcv 2903 . . . . . . . . 9 𝑖𝑆
103 nfcv 2903 . . . . . . . . 9 𝑖 D
104 nfcv 2903 . . . . . . . . . 10 𝑖𝑋
105 nfcv 2903 . . . . . . . . . . 11 𝑖𝑏
106105nfcprod1 15941 . . . . . . . . . 10 𝑖𝑖𝑏 𝐴
107104, 106nfmpt 5255 . . . . . . . . 9 𝑖(𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)
108102, 103, 107nfov 7461 . . . . . . . 8 𝑖(𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴))
109 nfcv 2903 . . . . . . . . . . 11 𝑖𝐶
110 nfcv 2903 . . . . . . . . . . 11 𝑖 ·
111 nfcv 2903 . . . . . . . . . . . 12 𝑖(𝑏 ∖ {𝑗})
112111nfcprod1 15941 . . . . . . . . . . 11 𝑖𝑖 ∈ (𝑏 ∖ {𝑗})𝐴
113109, 110, 112nfov 7461 . . . . . . . . . 10 𝑖(𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)
114105, 113nfsum 15724 . . . . . . . . 9 𝑖Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)
115104, 114nfmpt 5255 . . . . . . . 8 𝑖(𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
116108, 115nfeq 2917 . . . . . . 7 𝑖(𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
117101, 116nfan 1897 . . . . . 6 𝑖(((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)))
118 dvmptfprod.jph . . . . . . . . 9 𝑗𝜑
119 nfv 1912 . . . . . . . . 9 𝑗(𝑏 ∪ {𝑐}) ⊆ 𝐼
120118, 119nfan 1897 . . . . . . . 8 𝑗(𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)
121 nfv 1912 . . . . . . . 8 𝑗 ¬ 𝑐𝑏
122120, 121nfan 1897 . . . . . . 7 𝑗((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏)
123 nfcv 2903 . . . . . . . 8 𝑗(𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴))
124 nfcv 2903 . . . . . . . . 9 𝑗𝑋
125 nfcv 2903 . . . . . . . . . 10 𝑗𝑏
126125nfsum1 15723 . . . . . . . . 9 𝑗Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)
127124, 126nfmpt 5255 . . . . . . . 8 𝑗(𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
128123, 127nfeq 2917 . . . . . . 7 𝑗(𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))
129122, 128nfan 1897 . . . . . 6 𝑗(((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)))
130 nfcsb1v 3933 . . . . . 6 𝑖𝑐 / 𝑖𝐴
131 nfcsb1v 3933 . . . . . 6 𝑗𝑐 / 𝑗𝐶
132 simpl 482 . . . . . . . 8 ((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → 𝜑)
133132ad2antrr 726 . . . . . . 7 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → 𝜑)
134 dvmptfprod.a . . . . . . 7 ((𝜑𝑖𝐼𝑥𝑋) → 𝐴 ∈ ℂ)
135133, 134syl3an1 1162 . . . . . 6 (((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ 𝑖𝐼𝑥𝑋) → 𝐴 ∈ ℂ)
1361ad3antrrr 730 . . . . . . 7 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → 𝐼 ∈ Fin)
13783adantl 481 . . . . . . . 8 ((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → 𝑏𝐼)
138137ad2antrr 726 . . . . . . 7 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → 𝑏𝐼)
139136, 138ssfid 9299 . . . . . 6 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → 𝑏 ∈ Fin)
140 vex 3482 . . . . . . 7 𝑐 ∈ V
141140a1i 11 . . . . . 6 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → 𝑐 ∈ V)
142 simplr 769 . . . . . 6 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → ¬ 𝑐𝑏)
143 simpllr 776 . . . . . 6 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → (𝑏 ∪ {𝑐}) ⊆ 𝐼)
14464ad3antrrr 730 . . . . . 6 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → 𝑆 ∈ {ℝ, ℂ})
145133ad2antrr 726 . . . . . . 7 ((((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ 𝑥𝑋) ∧ 𝑗𝑏) → 𝜑)
146138ad2antrr 726 . . . . . . . 8 ((((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ 𝑥𝑋) ∧ 𝑗𝑏) → 𝑏𝐼)
147 simpr 484 . . . . . . . 8 ((((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ 𝑥𝑋) ∧ 𝑗𝑏) → 𝑗𝑏)
148146, 147sseldd 3996 . . . . . . 7 ((((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ 𝑥𝑋) ∧ 𝑗𝑏) → 𝑗𝐼)
149 simplr 769 . . . . . . 7 ((((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ 𝑥𝑋) ∧ 𝑗𝑏) → 𝑥𝑋)
150 nfv 1912 . . . . . . . . . 10 𝑖 𝑗𝐼
151 nfv 1912 . . . . . . . . . 10 𝑖 𝑥𝑋
15297, 150, 151nf3an 1899 . . . . . . . . 9 𝑖(𝜑𝑗𝐼𝑥𝑋)
153 nfv 1912 . . . . . . . . 9 𝑖 𝐶 ∈ ℂ
154152, 153nfim 1894 . . . . . . . 8 𝑖((𝜑𝑗𝐼𝑥𝑋) → 𝐶 ∈ ℂ)
155 eleq1w 2822 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝑖𝐼𝑗𝐼))
1561553anbi2d 1440 . . . . . . . . 9 (𝑖 = 𝑗 → ((𝜑𝑖𝐼𝑥𝑋) ↔ (𝜑𝑗𝐼𝑥𝑋)))
157 dvmptfprod.bc . . . . . . . . . 10 (𝑖 = 𝑗𝐵 = 𝐶)
158157eleq1d 2824 . . . . . . . . 9 (𝑖 = 𝑗 → (𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ))
159156, 158imbi12d 344 . . . . . . . 8 (𝑖 = 𝑗 → (((𝜑𝑖𝐼𝑥𝑋) → 𝐵 ∈ ℂ) ↔ ((𝜑𝑗𝐼𝑥𝑋) → 𝐶 ∈ ℂ)))
160 dvmptfprod.b . . . . . . . 8 ((𝜑𝑖𝐼𝑥𝑋) → 𝐵 ∈ ℂ)
161154, 159, 160chvarfv 2238 . . . . . . 7 ((𝜑𝑗𝐼𝑥𝑋) → 𝐶 ∈ ℂ)
162145, 148, 149, 161syl3anc 1370 . . . . . 6 ((((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ 𝑥𝑋) ∧ 𝑗𝑏) → 𝐶 ∈ ℂ)
163 simpr 484 . . . . . 6 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴)))
164132adantr 480 . . . . . . . 8 (((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑥𝑋) → 𝜑)
165 id 22 . . . . . . . . . 10 ((𝑏 ∪ {𝑐}) ⊆ 𝐼 → (𝑏 ∪ {𝑐}) ⊆ 𝐼)
166 vsnid 4668 . . . . . . . . . . 11 𝑐 ∈ {𝑐}
167 elun2 4193 . . . . . . . . . . 11 (𝑐 ∈ {𝑐} → 𝑐 ∈ (𝑏 ∪ {𝑐}))
168166, 167mp1i 13 . . . . . . . . . 10 ((𝑏 ∪ {𝑐}) ⊆ 𝐼𝑐 ∈ (𝑏 ∪ {𝑐}))
169165, 168sseldd 3996 . . . . . . . . 9 ((𝑏 ∪ {𝑐}) ⊆ 𝐼𝑐𝐼)
170169ad2antlr 727 . . . . . . . 8 (((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑥𝑋) → 𝑐𝐼)
171 simpr 484 . . . . . . . 8 (((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑥𝑋) → 𝑥𝑋)
172 nfv 1912 . . . . . . . . . . 11 𝑗 𝑐𝐼
173 nfv 1912 . . . . . . . . . . 11 𝑗 𝑥𝑋
174118, 172, 173nf3an 1899 . . . . . . . . . 10 𝑗(𝜑𝑐𝐼𝑥𝑋)
175131nfel1 2920 . . . . . . . . . 10 𝑗𝑐 / 𝑗𝐶 ∈ ℂ
176174, 175nfim 1894 . . . . . . . . 9 𝑗((𝜑𝑐𝐼𝑥𝑋) → 𝑐 / 𝑗𝐶 ∈ ℂ)
177 eleq1w 2822 . . . . . . . . . . 11 (𝑗 = 𝑐 → (𝑗𝐼𝑐𝐼))
1781773anbi2d 1440 . . . . . . . . . 10 (𝑗 = 𝑐 → ((𝜑𝑗𝐼𝑥𝑋) ↔ (𝜑𝑐𝐼𝑥𝑋)))
179 csbeq1a 3922 . . . . . . . . . . 11 (𝑗 = 𝑐𝐶 = 𝑐 / 𝑗𝐶)
180179eleq1d 2824 . . . . . . . . . 10 (𝑗 = 𝑐 → (𝐶 ∈ ℂ ↔ 𝑐 / 𝑗𝐶 ∈ ℂ))
181178, 180imbi12d 344 . . . . . . . . 9 (𝑗 = 𝑐 → (((𝜑𝑗𝐼𝑥𝑋) → 𝐶 ∈ ℂ) ↔ ((𝜑𝑐𝐼𝑥𝑋) → 𝑐 / 𝑗𝐶 ∈ ℂ)))
182176, 181, 161chvarfv 2238 . . . . . . . 8 ((𝜑𝑐𝐼𝑥𝑋) → 𝑐 / 𝑗𝐶 ∈ ℂ)
183164, 170, 171, 182syl3anc 1370 . . . . . . 7 (((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ 𝑥𝑋) → 𝑐 / 𝑗𝐶 ∈ ℂ)
184183ad4ant14 752 . . . . . 6 (((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ 𝑥𝑋) → 𝑐 / 𝑗𝐶 ∈ ℂ)
185118, 172nfan 1897 . . . . . . . . . 10 𝑗(𝜑𝑐𝐼)
186 nfcv 2903 . . . . . . . . . . 11 𝑗(𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴))
187124, 131nfmpt 5255 . . . . . . . . . . 11 𝑗(𝑥𝑋𝑐 / 𝑗𝐶)
188186, 187nfeq 2917 . . . . . . . . . 10 𝑗(𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑗𝐶)
189185, 188nfim 1894 . . . . . . . . 9 𝑗((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑗𝐶))
190177anbi2d 630 . . . . . . . . . 10 (𝑗 = 𝑐 → ((𝜑𝑗𝐼) ↔ (𝜑𝑐𝐼)))
191 csbeq1 3911 . . . . . . . . . . . . 13 (𝑗 = 𝑐𝑗 / 𝑖𝐴 = 𝑐 / 𝑖𝐴)
192191mpteq2dv 5250 . . . . . . . . . . . 12 (𝑗 = 𝑐 → (𝑥𝑋𝑗 / 𝑖𝐴) = (𝑥𝑋𝑐 / 𝑖𝐴))
193192oveq2d 7447 . . . . . . . . . . 11 (𝑗 = 𝑐 → (𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)) = (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)))
194179mpteq2dv 5250 . . . . . . . . . . 11 (𝑗 = 𝑐 → (𝑥𝑋𝐶) = (𝑥𝑋𝑐 / 𝑗𝐶))
195193, 194eqeq12d 2751 . . . . . . . . . 10 (𝑗 = 𝑐 → ((𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)) = (𝑥𝑋𝐶) ↔ (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑗𝐶)))
196190, 195imbi12d 344 . . . . . . . . 9 (𝑗 = 𝑐 → (((𝜑𝑗𝐼) → (𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)) = (𝑥𝑋𝐶)) ↔ ((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑗𝐶))))
19797, 150nfan 1897 . . . . . . . . . . 11 𝑖(𝜑𝑗𝐼)
198 nfcsb1v 3933 . . . . . . . . . . . . . 14 𝑖𝑗 / 𝑖𝐴
199104, 198nfmpt 5255 . . . . . . . . . . . . 13 𝑖(𝑥𝑋𝑗 / 𝑖𝐴)
200102, 103, 199nfov 7461 . . . . . . . . . . . 12 𝑖(𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴))
201 nfcv 2903 . . . . . . . . . . . 12 𝑖(𝑥𝑋𝐶)
202200, 201nfeq 2917 . . . . . . . . . . 11 𝑖(𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)) = (𝑥𝑋𝐶)
203197, 202nfim 1894 . . . . . . . . . 10 𝑖((𝜑𝑗𝐼) → (𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)) = (𝑥𝑋𝐶))
204155anbi2d 630 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((𝜑𝑖𝐼) ↔ (𝜑𝑗𝐼)))
205 csbeq1a 3922 . . . . . . . . . . . . . 14 (𝑖 = 𝑗𝐴 = 𝑗 / 𝑖𝐴)
206205mpteq2dv 5250 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (𝑥𝑋𝐴) = (𝑥𝑋𝑗 / 𝑖𝐴))
207206oveq2d 7447 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (𝑆 D (𝑥𝑋𝐴)) = (𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)))
208157mpteq2dv 5250 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (𝑥𝑋𝐵) = (𝑥𝑋𝐶))
209207, 208eqeq12d 2751 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵) ↔ (𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)) = (𝑥𝑋𝐶)))
210204, 209imbi12d 344 . . . . . . . . . 10 (𝑖 = 𝑗 → (((𝜑𝑖𝐼) → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵)) ↔ ((𝜑𝑗𝐼) → (𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)) = (𝑥𝑋𝐶))))
211 dvmptfprod.d . . . . . . . . . 10 ((𝜑𝑖𝐼) → (𝑆 D (𝑥𝑋𝐴)) = (𝑥𝑋𝐵))
212203, 210, 211chvarfv 2238 . . . . . . . . 9 ((𝜑𝑗𝐼) → (𝑆 D (𝑥𝑋𝑗 / 𝑖𝐴)) = (𝑥𝑋𝐶))
213189, 196, 212chvarfv 2238 . . . . . . . 8 ((𝜑𝑐𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑗𝐶))
214169, 213sylan2 593 . . . . . . 7 ((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑗𝐶))
215214ad2antrr 726 . . . . . 6 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → (𝑆 D (𝑥𝑋𝑐 / 𝑖𝐴)) = (𝑥𝑋𝑐 / 𝑗𝐶))
216 csbeq1a 3922 . . . . . 6 (𝑖 = 𝑐𝐴 = 𝑐 / 𝑖𝐴)
21796, 117, 129, 130, 131, 135, 139, 141, 142, 143, 144, 162, 163, 184, 215, 216, 179dvmptfprodlem 45900 . . . . 5 ((((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) ∧ ¬ 𝑐𝑏) ∧ (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴)))
21879, 80, 88, 217syl21anc 838 . . . 4 (((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) ∧ ((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) ∧ (𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼)) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴)))
2192183exp 1118 . . 3 ((𝑏 ∈ Fin ∧ ¬ 𝑐𝑏) → (((𝜑𝑏𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝑏 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝑏 (𝐶 · ∏𝑖 ∈ (𝑏 ∖ {𝑗})𝐴))) → ((𝜑 ∧ (𝑏 ∪ {𝑐}) ⊆ 𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖 ∈ (𝑏 ∪ {𝑐})𝐴)) = (𝑥𝑋 ↦ Σ𝑗 ∈ (𝑏 ∪ {𝑐})(𝐶 · ∏𝑖 ∈ ((𝑏 ∪ {𝑐}) ∖ {𝑗})𝐴)))))
22017, 31, 45, 59, 78, 219findcard2s 9204 . 2 (𝐼 ∈ Fin → ((𝜑𝐼𝐼) → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴))))
2211, 3, 220sylc 65 1 (𝜑 → (𝑆 D (𝑥𝑋 ↦ ∏𝑖𝐼 𝐴)) = (𝑥𝑋 ↦ Σ𝑗𝐼 (𝐶 · ∏𝑖 ∈ (𝐼 ∖ {𝑗})𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1086   = wceq 1537  wnf 1780  wcel 2106  Vcvv 3478  csb 3908  cdif 3960  cun 3961  wss 3963  c0 4339  {csn 4631  {cpr 4633  cmpt 5231  cfv 6563  (class class class)co 7431  Fincfn 8984  cc 11151  cr 11152  0cc0 11153  1c1 11154   · cmul 11158  Σcsu 15719  cprod 15936  t crest 17467  TopOpenctopn 17468  fldccnfld 21382   D cdv 25913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231  ax-addf 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-fi 9449  df-sup 9480  df-inf 9481  df-oi 9548  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-icc 13391  df-fz 13545  df-fzo 13692  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-clim 15521  df-sum 15720  df-prod 15937  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-rest 17469  df-topn 17470  df-0g 17488  df-gsum 17489  df-topgen 17490  df-pt 17491  df-prds 17494  df-xrs 17549  df-qtop 17554  df-imas 17555  df-xps 17557  df-mre 17631  df-mrc 17632  df-acs 17634  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-submnd 18810  df-mulg 19099  df-cntz 19348  df-cmn 19815  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-fbas 21379  df-fg 21380  df-cnfld 21383  df-top 22916  df-topon 22933  df-topsp 22955  df-bases 22969  df-cld 23043  df-ntr 23044  df-cls 23045  df-nei 23122  df-lp 23160  df-perf 23161  df-cn 23251  df-cnp 23252  df-haus 23339  df-tx 23586  df-hmeo 23779  df-fil 23870  df-fm 23962  df-flim 23963  df-flf 23964  df-xms 24346  df-ms 24347  df-tms 24348  df-cncf 24918  df-limc 25916  df-dv 25917
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator