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