This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) )