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 a1d ⊢ ( 𝑎 = 𝐼 → ( 𝑗 ∈ 𝐼 → ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) )
66 65 ralrimiv ⊢ ( 𝑎 = 𝐼 → ∀ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) )
67 66 sumeq2d ⊢ ( 𝑎 = 𝐼 → Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) )
68 61 67 eqtrd ⊢ ( 𝑎 = 𝐼 → Σ 𝑗 ∈ 𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) )
69 68 mpteq2dv ⊢ ( 𝑎 = 𝐼 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) )
70 60 69 eqeq12d ⊢ ( 𝑎 = 𝐼 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) ) )
71 57 70 imbi12d ⊢ ( 𝑎 = 𝐼 → ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑎 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑎 ∖ { 𝑗 } ) 𝐴 ) ) ) ↔ ( ( 𝜑 ∧ 𝐼 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) ) ) )
72 prod0 ⊢ ∏ 𝑖 ∈ ∅ 𝐴 = 1
73 72 mpteq2i ⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 1 )
74 73 oveq2i ⊢ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 1 ) )
75 74 a1i ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 1 ) ) )
76 4 oveq1i ⊢ ( 𝐾 ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
77 3 76 eqtri ⊢ 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
78 6 77 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
79 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
80 5 78 79 dvmptconst ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
81 sum0 ⊢ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) = 0
82 81 eqcomi ⊢ 0 = Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 )
83 82 mpteq2i ⊢ ( 𝑥 ∈ 𝑋 ↦ 0 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) )
84 83 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 0 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) )
85 75 80 84 3eqtrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) )
86 85 adantr ⊢ ( ( 𝜑 ∧ ∅ ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ∅ ( 𝐶 · ∏ 𝑖 ∈ ( ∅ ∖ { 𝑗 } ) 𝐴 ) ) )
87 simp3 ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) )
88 simp1r ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ¬ 𝑐 ∈ 𝑏 )
89 simpl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → 𝜑 )
90 ssun1 ⊢ 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } )
91 sstr2 ⊢ ( 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → 𝑏 ⊆ 𝐼 ) )
92 90 91 ax-mp ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → 𝑏 ⊆ 𝐼 )
93 92 adantl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → 𝑏 ⊆ 𝐼 )
94 89 93 jca ⊢ ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) )
95 94 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) )
96 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) )
97 95 96 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
98 97 3adant1 ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
99 nfv ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 )
100 nfcv ⊢ Ⅎ 𝑥 𝑆
101 nfcv ⊢ Ⅎ 𝑥 D
102 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 )
103 100 101 102 nfov ⊢ Ⅎ 𝑥 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) )
104 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
105 103 104 nfeq ⊢ Ⅎ 𝑥 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
106 99 105 nfan ⊢ Ⅎ 𝑥 ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
107 nfv ⊢ Ⅎ 𝑖 ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼
108 1 107 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
109 nfv ⊢ Ⅎ 𝑖 ¬ 𝑐 ∈ 𝑏
110 108 109 nfan ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 )
111 nfcv ⊢ Ⅎ 𝑖 𝑆
112 nfcv ⊢ Ⅎ 𝑖 D
113 nfcv ⊢ Ⅎ 𝑖 𝑋
114 nfcv ⊢ Ⅎ 𝑖 𝑏
115 114 nfcprod1 ⊢ Ⅎ 𝑖 ∏ 𝑖 ∈ 𝑏 𝐴
116 113 115 nfmpt ⊢ Ⅎ 𝑖 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 )
117 111 112 116 nfov ⊢ Ⅎ 𝑖 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) )
118 nfcv ⊢ Ⅎ 𝑖 𝐶
119 nfcv ⊢ Ⅎ 𝑖 ·
120 nfcv ⊢ Ⅎ 𝑖 ( 𝑏 ∖ { 𝑗 } )
121 120 nfcprod1 ⊢ Ⅎ 𝑖 ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴
122 118 119 121 nfov ⊢ Ⅎ 𝑖 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 )
123 114 122 nfsum ⊢ Ⅎ 𝑖 Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 )
124 113 123 nfmpt ⊢ Ⅎ 𝑖 ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
125 117 124 nfeq ⊢ Ⅎ 𝑖 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
126 110 125 nfan ⊢ Ⅎ 𝑖 ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
127 nfv ⊢ Ⅎ 𝑗 ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼
128 2 127 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
129 nfv ⊢ Ⅎ 𝑗 ¬ 𝑐 ∈ 𝑏
130 128 129 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 )
131 nfcv ⊢ Ⅎ 𝑗 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) )
132 nfcv ⊢ Ⅎ 𝑗 𝑋
133 nfcv ⊢ Ⅎ 𝑗 𝑏
134 133 nfsum1 ⊢ Ⅎ 𝑗 Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 )
135 132 134 nfmpt ⊢ Ⅎ 𝑗 ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
136 131 135 nfeq ⊢ Ⅎ 𝑗 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) )
137 130 136 nfan ⊢ Ⅎ 𝑗 ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
138 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑐 / 𝑖 ⦌ 𝐴
139 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑐 / 𝑗 ⦌ 𝐶
140 89 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝜑 )
141 140 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝜑 )
142 simp2 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝑖 ∈ 𝐼 )
143 simp3 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
144 141 142 143 8 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
145 140 7 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝐼 ∈ Fin )
146 93 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝑏 ⊆ 𝐼 )
147 ssfi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑏 ⊆ 𝐼 ) → 𝑏 ∈ Fin )
148 145 146 147 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝑏 ∈ Fin )
149 vex ⊢ 𝑐 ∈ V
150 149 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝑐 ∈ V )
151 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ¬ 𝑐 ∈ 𝑏 )
152 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
153 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → 𝑆 ∈ { ℝ , ℂ } )
154 140 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝑏 ) → 𝜑 )
155 146 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝑏 ) → 𝑏 ⊆ 𝐼 )
156 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝑏 ) → 𝑗 ∈ 𝑏 )
157 155 156 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝑏 ) → 𝑗 ∈ 𝐼 )
158 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝑏 ) → 𝑥 ∈ 𝑋 )
159 nfv ⊢ Ⅎ 𝑖 𝑗 ∈ 𝐼
160 nfv ⊢ Ⅎ 𝑖 𝑥 ∈ 𝑋
161 1 159 160 nf3an ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑗 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 )
162 nfv ⊢ Ⅎ 𝑖 𝐶 ∈ ℂ
163 161 162 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
164 eleq1w ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ∈ 𝐼 ↔ 𝑗 ∈ 𝐼 ) )
165 164 3anbi2d ⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) )
166 11 eleq1d ⊢ ( 𝑖 = 𝑗 → ( 𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
167 165 166 imbi12d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ ) ) )
168 163 167 9 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
169 154 157 158 168 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝑏 ) → 𝐶 ∈ ℂ )
170 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) )
171 89 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → 𝜑 )
172 id ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
173 149 snid ⊢ 𝑐 ∈ { 𝑐 }
174 elun2 ⊢ ( 𝑐 ∈ { 𝑐 } → 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } ) )
175 173 174 ax-mp ⊢ 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } )
176 175 a1i ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → 𝑐 ∈ ( 𝑏 ∪ { 𝑐 } ) )
177 172 176 sseldd ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → 𝑐 ∈ 𝐼 )
178 177 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑐 ∈ 𝐼 )
179 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
180 nfv ⊢ Ⅎ 𝑗 𝑐 ∈ 𝐼
181 nfv ⊢ Ⅎ 𝑗 𝑥 ∈ 𝑋
182 2 180 181 nf3an ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑐 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 )
183 nfcv ⊢ Ⅎ 𝑗 ℂ
184 139 183 nfel ⊢ Ⅎ 𝑗 ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ∈ ℂ
185 182 184 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ∈ ℂ )
186 eleq1w ⊢ ( 𝑗 = 𝑐 → ( 𝑗 ∈ 𝐼 ↔ 𝑐 ∈ 𝐼 ) )
187 186 3anbi2d ⊢ ( 𝑗 = 𝑐 → ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑐 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) )
188 csbeq1a ⊢ ( 𝑗 = 𝑐 → 𝐶 = ⦋ 𝑐 / 𝑗 ⦌ 𝐶 )
189 188 eleq1d ⊢ ( 𝑗 = 𝑐 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
190 187 189 imbi12d ⊢ ( 𝑗 = 𝑐 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ∈ ℂ ) ) )
191 185 190 168 chvarfv ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ∈ ℂ )
192 171 178 179 191 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ∈ ℂ )
193 192 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ∈ ℂ )
194 193 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ∈ ℂ )
195 2 180 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑐 ∈ 𝐼 )
196 nfcv ⊢ Ⅎ 𝑗 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) )
197 132 139 nfmpt ⊢ Ⅎ 𝑗 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 )
198 196 197 nfeq ⊢ Ⅎ 𝑗 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 )
199 195 198 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ) )
200 186 anbi2d ⊢ ( 𝑗 = 𝑐 → ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ↔ ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ) )
201 csbeq1a ⊢ ( 𝑗 = 𝑐 → ⦋ 𝑗 / 𝑖 ⦌ 𝐴 = ⦋ 𝑐 / 𝑗 ⦌ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 )
202 csbcow ⊢ ⦋ 𝑐 / 𝑗 ⦌ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ 𝐴
203 202 a1i ⊢ ( 𝑗 = 𝑐 → ⦋ 𝑐 / 𝑗 ⦌ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ 𝐴 )
204 201 203 eqtrd ⊢ ( 𝑗 = 𝑐 → ⦋ 𝑗 / 𝑖 ⦌ 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ 𝐴 )
205 204 mpteq2dv ⊢ ( 𝑗 = 𝑐 → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) )
206 205 oveq2d ⊢ ( 𝑗 = 𝑐 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) )
207 188 mpteq2dv ⊢ ( 𝑗 = 𝑐 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ) )
208 206 207 eqeq12d ⊢ ( 𝑗 = 𝑐 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ) ) )
209 200 208 imbi12d ⊢ ( 𝑗 = 𝑐 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ↔ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ) ) ) )
210 1 159 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑗 ∈ 𝐼 )
211 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑗 / 𝑖 ⦌ 𝐴
212 113 211 nfmpt ⊢ Ⅎ 𝑖 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 )
213 111 112 212 nfov ⊢ Ⅎ 𝑖 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) )
214 nfcv ⊢ Ⅎ 𝑖 ( 𝑥 ∈ 𝑋 ↦ 𝐶 )
215 213 214 nfeq ⊢ Ⅎ 𝑖 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 )
216 210 215 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
217 164 anbi2d ⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ) )
218 csbeq1a ⊢ ( 𝑖 = 𝑗 → 𝐴 = ⦋ 𝑗 / 𝑖 ⦌ 𝐴 )
219 218 mpteq2dv ⊢ ( 𝑖 = 𝑗 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) )
220 219 oveq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) )
221 11 idi ⊢ ( 𝑖 = 𝑗 → 𝐵 = 𝐶 )
222 221 mpteq2dv ⊢ ( 𝑖 = 𝑗 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
223 220 222 eqeq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) )
224 217 223 imbi12d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ) )
225 216 224 10 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑗 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
226 199 209 225 chvarfv ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ) )
227 177 226 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ) )
228 227 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑗 ⦌ 𝐶 ) )
229 csbeq1a ⊢ ( 𝑖 = 𝑐 → 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ 𝐴 )
230 106 126 137 138 139 144 148 150 151 152 153 169 170 194 228 229 188 dvmptfprodlem ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) )
231 87 88 98 230 syl21anc ⊢ ( ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) ∧ ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) )
232 231 3exp ⊢ ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) → ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝑏 ( 𝐶 · ∏ 𝑖 ∈ ( 𝑏 ∖ { 𝑗 } ) 𝐴 ) ) ) → ( ( 𝜑 ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ( 𝑏 ∪ { 𝑐 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝑏 ∪ { 𝑐 } ) ∖ { 𝑗 } ) 𝐴 ) ) ) ) )
233 27 41 55 71 86 232 findcard2s ⊢ ( 𝐼 ∈ Fin → ( ( 𝜑 ∧ 𝐼 ⊆ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) ) )
234 7 13 233 sylc ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝐼 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐼 ∖ { 𝑗 } ) 𝐴 ) ) )