Metamath Proof Explorer


Theorem dvmptfprod

Description: Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses 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 dvmptfprod ( 𝜑 → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝐼 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 dvmptfprod.iph 𝑖 𝜑
2 dvmptfprod.jph 𝑗 𝜑
3 dvmptfprod.j 𝐽 = ( 𝐾t 𝑆 )
4 dvmptfprod.k 𝐾 = ( TopOpen ‘ ℂfld )
5 dvmptfprod.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
6 dvmptfprod.x ( 𝜑𝑋𝐽 )
7 dvmptfprod.i ( 𝜑𝐼 ∈ Fin )
8 dvmptfprod.a ( ( 𝜑𝑖𝐼𝑥𝑋 ) → 𝐴 ∈ ℂ )
9 dvmptfprod.b ( ( 𝜑𝑖𝐼𝑥𝑋 ) → 𝐵 ∈ ℂ )
10 dvmptfprod.d ( ( 𝜑𝑖𝐼 ) → ( 𝑆 D ( 𝑥𝑋𝐴 ) ) = ( 𝑥𝑋𝐵 ) )
11 dvmptfprod.bc ( 𝑖 = 𝑗𝐵 = 𝐶 )
12 ssid 𝐼𝐼
13 12 jctr ( 𝜑 → ( 𝜑𝐼𝐼 ) )
14 sseq1 ( 𝑎 = ∅ → ( 𝑎𝐼 ↔ ∅ ⊆ 𝐼 ) )
15 14 anbi2d ( 𝑎 = ∅ → ( ( 𝜑𝑎𝐼 ) ↔ ( 𝜑 ∧ ∅ ⊆ 𝐼 ) ) )
16 prodeq1 ( 𝑎 = ∅ → ∏ 𝑖𝑎 𝐴 = ∏ 𝑖 ∈ ∅ 𝐴 )
17 16 mpteq2dv ( 𝑎 = ∅ → ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) = ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) )
18 17 oveq2d ( 𝑎 = ∅ → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) )
19 sumeq1 ( 𝑎 = ∅ → Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) )
20 difeq1 ( 𝑎 = ∅ → ( 𝑎 ∖ { 𝑗 } ) = ( ∅ ∖ { 𝑗 } ) )
21 20 prodeq1d ( 𝑎 = ∅ → ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 = ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 )
22 21 oveq2d ( 𝑎 = ∅ → ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) )
23 22 sumeq2sdv ( 𝑎 = ∅ → Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) )
24 19 23 eqtrd ( 𝑎 = ∅ → Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) )
25 24 mpteq2dv ( 𝑎 = ∅ → ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) )
26 18 25 eqeq12d ( 𝑎 = ∅ → ( ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ↔ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) ) )
27 15 26 imbi12d ( 𝑎 = ∅ → ( ( ( 𝜑𝑎𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ) ↔ ( ( 𝜑 ∧ ∅ ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) ) ) )
28 sseq1 ( 𝑎 = 𝑏 → ( 𝑎𝐼𝑏𝐼 ) )
29 28 anbi2d ( 𝑎 = 𝑏 → ( ( 𝜑𝑎𝐼 ) ↔ ( 𝜑𝑏𝐼 ) ) )
30 prodeq1 ( 𝑎 = 𝑏 → ∏ 𝑖𝑎 𝐴 = ∏ 𝑖𝑏 𝐴 )
31 30 mpteq2dv ( 𝑎 = 𝑏 → ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) = ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) )
32 31 oveq2d ( 𝑎 = 𝑏 → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) )
33 sumeq1 ( 𝑎 = 𝑏 → Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) )
34 difeq1 ( 𝑎 = 𝑏 → ( 𝑎 ∖ { 𝑗 } ) = ( 𝑏 ∖ { 𝑗 } ) )
35 34 prodeq1d ( 𝑎 = 𝑏 → ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 = ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 )
36 35 oveq2d ( 𝑎 = 𝑏 → ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
37 36 sumeq2sdv ( 𝑎 = 𝑏 → Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
38 33 37 eqtrd ( 𝑎 = 𝑏 → Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
39 38 mpteq2dv ( 𝑎 = 𝑏 → ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
40 32 39 eqeq12d ( 𝑎 = 𝑏 → ( ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ↔ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) )
41 29 40 imbi12d ( 𝑎 = 𝑏 → ( ( ( 𝜑𝑎𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ) ↔ ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ) )
42 sseq1 ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑎𝐼 ↔ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) )
43 42 anbi2d ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝜑𝑎𝐼 ) ↔ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) )
44 prodeq1 ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ∏ 𝑖𝑎 𝐴 = ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 )
45 44 mpteq2dv ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) = ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) )
46 45 oveq2d ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) )
47 sumeq1 ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) )
48 difeq1 ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑎 ∖ { 𝑗 } ) = ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) )
49 48 prodeq1d ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 = ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 )
50 49 oveq2d ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) )
51 50 sumeq2sdv ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) )
52 47 51 eqtrd ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) )
53 52 mpteq2dv ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) )
54 46 53 eqeq12d ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ↔ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) ) )
55 43 54 imbi12d ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( ( 𝜑𝑎𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) ) ) )
56 sseq1 ( 𝑎 = 𝐼 → ( 𝑎𝐼𝐼𝐼 ) )
57 56 anbi2d ( 𝑎 = 𝐼 → ( ( 𝜑𝑎𝐼 ) ↔ ( 𝜑𝐼𝐼 ) ) )
58 prodeq1 ( 𝑎 = 𝐼 → ∏ 𝑖𝑎 𝐴 = ∏ 𝑖𝐼 𝐴 )
59 58 mpteq2dv ( 𝑎 = 𝐼 → ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) = ( 𝑥𝑋 ↦ ∏ 𝑖𝐼 𝐴 ) )
60 59 oveq2d ( 𝑎 = 𝐼 → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝐼 𝐴 ) ) )
61 sumeq1 ( 𝑎 = 𝐼 → Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) )
62 difeq1 ( 𝑎 = 𝐼 → ( 𝑎 ∖ { 𝑗 } ) = ( 𝐼 ∖ { 𝑗 } ) )
63 62 prodeq1d ( 𝑎 = 𝐼 → ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 = ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 )
64 63 oveq2d ( 𝑎 = 𝐼 → ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) )
65 64 sumeq2sdv ( 𝑎 = 𝐼 → Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) )
66 61 65 eqtrd ( 𝑎 = 𝐼 → Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) )
67 66 mpteq2dv ( 𝑎 = 𝐼 → ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) )
68 60 67 eqeq12d ( 𝑎 = 𝐼 → ( ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ↔ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝐼 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) ) )
69 57 68 imbi12d ( 𝑎 = 𝐼 → ( ( ( 𝜑𝑎𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑎 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ) ↔ ( ( 𝜑𝐼𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝐼 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) ) ) )
70 prod0 𝑖 ∈ ∅ 𝐴 = 1
71 70 mpteq2i ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) = ( 𝑥𝑋 ↦ 1 )
72 71 oveq2i ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑆 D ( 𝑥𝑋 ↦ 1 ) )
73 72 a1i ( 𝜑 → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑆 D ( 𝑥𝑋 ↦ 1 ) ) )
74 4 oveq1i ( 𝐾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
75 3 74 eqtri 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
76 6 75 eleqtrdi ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
77 1cnd ( 𝜑 → 1 ∈ ℂ )
78 5 76 77 dvmptconst ( 𝜑 → ( 𝑆 D ( 𝑥𝑋 ↦ 1 ) ) = ( 𝑥𝑋 ↦ 0 ) )
79 sum0 Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) = 0
80 79 eqcomi 0 = Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 )
81 80 mpteq2i ( 𝑥𝑋 ↦ 0 ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) )
82 81 a1i ( 𝜑 → ( 𝑥𝑋 ↦ 0 ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) )
83 73 78 82 3eqtrd ( 𝜑 → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) )
84 83 adantr ( ( 𝜑 ∧ ∅ ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) )
85 simp3 ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐𝑏 ) ∧ ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) )
86 simp1r ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐𝑏 ) ∧ ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ¬ 𝑐𝑏 )
87 ssun1 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } )
88 sstr2 ( 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼𝑏𝐼 ) )
89 87 88 ax-mp ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼𝑏𝐼 )
90 89 anim2i ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝜑𝑏𝐼 ) )
91 90 adantl ( ( ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝜑𝑏𝐼 ) )
92 simpl ( ( ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) )
93 91 92 mpd ( ( ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
94 93 3adant1 ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐𝑏 ) ∧ ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
95 nfv 𝑥 ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 )
96 nfcv 𝑥 𝑆
97 nfcv 𝑥 D
98 nfmpt1 𝑥 ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 )
99 96 97 98 nfov 𝑥 ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) )
100 nfmpt1 𝑥 ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
101 99 100 nfeq 𝑥 ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
102 95 101 nfan 𝑥 ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
103 nfv 𝑖 ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼
104 1 103 nfan 𝑖 ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
105 nfv 𝑖 ¬ 𝑐𝑏
106 104 105 nfan 𝑖 ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 )
107 nfcv 𝑖 𝑆
108 nfcv 𝑖 D
109 nfcv 𝑖 𝑋
110 nfcv 𝑖 𝑏
111 110 nfcprod1 𝑖𝑖𝑏 𝐴
112 109 111 nfmpt 𝑖 ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 )
113 107 108 112 nfov 𝑖 ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) )
114 nfcv 𝑖 𝐶
115 nfcv 𝑖 ·
116 nfcv 𝑖 ( 𝑏 ∖ { 𝑗 } )
117 116 nfcprod1 𝑖𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴
118 114 115 117 nfov 𝑖 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 )
119 110 118 nfsum 𝑖 Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 )
120 109 119 nfmpt 𝑖 ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
121 113 120 nfeq 𝑖 ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
122 106 121 nfan 𝑖 ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
123 nfv 𝑗 ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼
124 2 123 nfan 𝑗 ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
125 nfv 𝑗 ¬ 𝑐𝑏
126 124 125 nfan 𝑗 ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 )
127 nfcv 𝑗 ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) )
128 nfcv 𝑗 𝑋
129 nfcv 𝑗 𝑏
130 129 nfsum1 𝑗 Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 )
131 128 130 nfmpt 𝑗 ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
132 127 131 nfeq 𝑗 ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
133 126 132 nfan 𝑗 ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
134 nfcsb1v 𝑖 𝑐 / 𝑖 𝐴
135 nfcsb1v 𝑗 𝑐 / 𝑗 𝐶
136 simpl ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → 𝜑 )
137 136 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝜑 )
138 137 8 syl3an1 ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑖𝐼𝑥𝑋 ) → 𝐴 ∈ ℂ )
139 7 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝐼 ∈ Fin )
140 89 adantl ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → 𝑏𝐼 )
141 140 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝑏𝐼 )
142 139 141 ssfid ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝑏 ∈ Fin )
143 vex 𝑐 ∈ V
144 143 a1i ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝑐 ∈ V )
145 simplr ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ¬ 𝑐𝑏 )
146 simpllr ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
147 5 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝑆 ∈ { ℝ , ℂ } )
148 137 ad2antrr ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥𝑋 ) ∧ 𝑗𝑏 ) → 𝜑 )
149 141 ad2antrr ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥𝑋 ) ∧ 𝑗𝑏 ) → 𝑏𝐼 )
150 simpr ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥𝑋 ) ∧ 𝑗𝑏 ) → 𝑗𝑏 )
151 149 150 sseldd ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥𝑋 ) ∧ 𝑗𝑏 ) → 𝑗𝐼 )
152 simplr ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥𝑋 ) ∧ 𝑗𝑏 ) → 𝑥𝑋 )
153 nfv 𝑖 𝑗𝐼
154 nfv 𝑖 𝑥𝑋
155 1 153 154 nf3an 𝑖 ( 𝜑𝑗𝐼𝑥𝑋 )
156 nfv 𝑖 𝐶 ∈ ℂ
157 155 156 nfim 𝑖 ( ( 𝜑𝑗𝐼𝑥𝑋 ) → 𝐶 ∈ ℂ )
158 eleq1w ( 𝑖 = 𝑗 → ( 𝑖𝐼𝑗𝐼 ) )
159 158 3anbi2d ( 𝑖 = 𝑗 → ( ( 𝜑𝑖𝐼𝑥𝑋 ) ↔ ( 𝜑𝑗𝐼𝑥𝑋 ) ) )
160 11 eleq1d ( 𝑖 = 𝑗 → ( 𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
161 159 160 imbi12d ( 𝑖 = 𝑗 → ( ( ( 𝜑𝑖𝐼𝑥𝑋 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑𝑗𝐼𝑥𝑋 ) → 𝐶 ∈ ℂ ) ) )
162 157 161 9 chvarfv ( ( 𝜑𝑗𝐼𝑥𝑋 ) → 𝐶 ∈ ℂ )
163 148 151 152 162 syl3anc ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥𝑋 ) ∧ 𝑗𝑏 ) → 𝐶 ∈ ℂ )
164 simpr ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
165 136 adantr ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑥𝑋 ) → 𝜑 )
166 id ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
167 vsnid 𝑐 ∈ { 𝑐 }
168 elun2 ( 𝑐 ∈ { 𝑐 } → 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } ) )
169 167 168 mp1i ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼𝑐 ∈ ( 𝑏 ∪ { 𝑐 } ) )
170 166 169 sseldd ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼𝑐𝐼 )
171 170 ad2antlr ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑥𝑋 ) → 𝑐𝐼 )
172 simpr ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑥𝑋 ) → 𝑥𝑋 )
173 nfv 𝑗 𝑐𝐼
174 nfv 𝑗 𝑥𝑋
175 2 173 174 nf3an 𝑗 ( 𝜑𝑐𝐼𝑥𝑋 )
176 135 nfel1 𝑗 𝑐 / 𝑗 𝐶 ∈ ℂ
177 175 176 nfim 𝑗 ( ( 𝜑𝑐𝐼𝑥𝑋 ) → 𝑐 / 𝑗 𝐶 ∈ ℂ )
178 eleq1w ( 𝑗 = 𝑐 → ( 𝑗𝐼𝑐𝐼 ) )
179 178 3anbi2d ( 𝑗 = 𝑐 → ( ( 𝜑𝑗𝐼𝑥𝑋 ) ↔ ( 𝜑𝑐𝐼𝑥𝑋 ) ) )
180 csbeq1a ( 𝑗 = 𝑐𝐶 = 𝑐 / 𝑗 𝐶 )
181 180 eleq1d ( 𝑗 = 𝑐 → ( 𝐶 ∈ ℂ ↔ 𝑐 / 𝑗 𝐶 ∈ ℂ ) )
182 179 181 imbi12d ( 𝑗 = 𝑐 → ( ( ( 𝜑𝑗𝐼𝑥𝑋 ) → 𝐶 ∈ ℂ ) ↔ ( ( 𝜑𝑐𝐼𝑥𝑋 ) → 𝑐 / 𝑗 𝐶 ∈ ℂ ) ) )
183 177 182 162 chvarfv ( ( 𝜑𝑐𝐼𝑥𝑋 ) → 𝑐 / 𝑗 𝐶 ∈ ℂ )
184 165 171 172 183 syl3anc ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑥𝑋 ) → 𝑐 / 𝑗 𝐶 ∈ ℂ )
185 184 ad4ant14 ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥𝑋 ) → 𝑐 / 𝑗 𝐶 ∈ ℂ )
186 2 173 nfan 𝑗 ( 𝜑𝑐𝐼 )
187 nfcv 𝑗 ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) )
188 128 135 nfmpt 𝑗 ( 𝑥𝑋 𝑐 / 𝑗 𝐶 )
189 187 188 nfeq 𝑗 ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) ) = ( 𝑥𝑋 𝑐 / 𝑗 𝐶 )
190 186 189 nfim 𝑗 ( ( 𝜑𝑐𝐼 ) → ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) ) = ( 𝑥𝑋 𝑐 / 𝑗 𝐶 ) )
191 178 anbi2d ( 𝑗 = 𝑐 → ( ( 𝜑𝑗𝐼 ) ↔ ( 𝜑𝑐𝐼 ) ) )
192 csbeq1 ( 𝑗 = 𝑐 𝑗 / 𝑖 𝐴 = 𝑐 / 𝑖 𝐴 )
193 192 mpteq2dv ( 𝑗 = 𝑐 → ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) = ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) )
194 193 oveq2d ( 𝑗 = 𝑐 → ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) = ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) ) )
195 180 mpteq2dv ( 𝑗 = 𝑐 → ( 𝑥𝑋𝐶 ) = ( 𝑥𝑋 𝑐 / 𝑗 𝐶 ) )
196 194 195 eqeq12d ( 𝑗 = 𝑐 → ( ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) = ( 𝑥𝑋𝐶 ) ↔ ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) ) = ( 𝑥𝑋 𝑐 / 𝑗 𝐶 ) ) )
197 191 196 imbi12d ( 𝑗 = 𝑐 → ( ( ( 𝜑𝑗𝐼 ) → ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) = ( 𝑥𝑋𝐶 ) ) ↔ ( ( 𝜑𝑐𝐼 ) → ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) ) = ( 𝑥𝑋 𝑐 / 𝑗 𝐶 ) ) ) )
198 1 153 nfan 𝑖 ( 𝜑𝑗𝐼 )
199 nfcsb1v 𝑖 𝑗 / 𝑖 𝐴
200 109 199 nfmpt 𝑖 ( 𝑥𝑋 𝑗 / 𝑖 𝐴 )
201 107 108 200 nfov 𝑖 ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) )
202 nfcv 𝑖 ( 𝑥𝑋𝐶 )
203 201 202 nfeq 𝑖 ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) = ( 𝑥𝑋𝐶 )
204 198 203 nfim 𝑖 ( ( 𝜑𝑗𝐼 ) → ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) = ( 𝑥𝑋𝐶 ) )
205 158 anbi2d ( 𝑖 = 𝑗 → ( ( 𝜑𝑖𝐼 ) ↔ ( 𝜑𝑗𝐼 ) ) )
206 csbeq1a ( 𝑖 = 𝑗𝐴 = 𝑗 / 𝑖 𝐴 )
207 206 mpteq2dv ( 𝑖 = 𝑗 → ( 𝑥𝑋𝐴 ) = ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) )
208 207 oveq2d ( 𝑖 = 𝑗 → ( 𝑆 D ( 𝑥𝑋𝐴 ) ) = ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) )
209 11 mpteq2dv ( 𝑖 = 𝑗 → ( 𝑥𝑋𝐵 ) = ( 𝑥𝑋𝐶 ) )
210 208 209 eqeq12d ( 𝑖 = 𝑗 → ( ( 𝑆 D ( 𝑥𝑋𝐴 ) ) = ( 𝑥𝑋𝐵 ) ↔ ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) = ( 𝑥𝑋𝐶 ) ) )
211 205 210 imbi12d ( 𝑖 = 𝑗 → ( ( ( 𝜑𝑖𝐼 ) → ( 𝑆 D ( 𝑥𝑋𝐴 ) ) = ( 𝑥𝑋𝐵 ) ) ↔ ( ( 𝜑𝑗𝐼 ) → ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) = ( 𝑥𝑋𝐶 ) ) ) )
212 204 211 10 chvarfv ( ( 𝜑𝑗𝐼 ) → ( 𝑆 D ( 𝑥𝑋 𝑗 / 𝑖 𝐴 ) ) = ( 𝑥𝑋𝐶 ) )
213 190 197 212 chvarfv ( ( 𝜑𝑐𝐼 ) → ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) ) = ( 𝑥𝑋 𝑐 / 𝑗 𝐶 ) )
214 170 213 sylan2 ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) ) = ( 𝑥𝑋 𝑐 / 𝑗 𝐶 ) )
215 214 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( 𝑆 D ( 𝑥𝑋 𝑐 / 𝑖 𝐴 ) ) = ( 𝑥𝑋 𝑐 / 𝑗 𝐶 ) )
216 csbeq1a ( 𝑖 = 𝑐𝐴 = 𝑐 / 𝑖 𝐴 )
217 102 122 133 134 135 138 142 144 145 146 147 163 164 185 215 216 180 dvmptfprodlem ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐𝑏 ) ∧ ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) )
218 85 86 94 217 syl21anc ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐𝑏 ) ∧ ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) )
219 218 3exp ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐𝑏 ) → ( ( ( 𝜑𝑏𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝑏 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) ) ) )
220 27 41 55 69 84 219 findcard2s ( 𝐼 ∈ Fin → ( ( 𝜑𝐼𝐼 ) → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝐼 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) ) )
221 7 13 220 sylc ( 𝜑 → ( 𝑆 D ( 𝑥𝑋 ↦ ∏ 𝑖𝐼 𝐴 ) ) = ( 𝑥𝑋 ↦ Σ 𝑗𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) )