Metamath Proof Explorer

Theorem dvmptfsum

Description: Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014)

Ref Expression
Hypotheses dvmptfsum.j ⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
dvmptfsum.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
dvmptfsum.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptfsum.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
dvmptfsum.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
dvmptfsum.a ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptfsum.b ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
dvmptfsum.d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
Assertion dvmptfsum ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dvmptfsum.j ⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
2 dvmptfsum.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3 dvmptfsum.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
4 dvmptfsum.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
5 dvmptfsum.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
6 dvmptfsum.a ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
7 dvmptfsum.b ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
8 dvmptfsum.d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
9 ssid ⊢ 𝐼 ⊆ 𝐼
10 sseq1 ⊢ ( 𝑎 = ∅ → ( 𝑎 ⊆ 𝐼 ↔ ∅ ⊆ 𝐼 ) )
11 sumeq1 ⊢ ( 𝑎 = ∅ → Σ 𝑖 ∈ 𝑎 𝐴 = Σ 𝑖 ∈ ∅ 𝐴 )
12 11 mpteq2dv ⊢ ( 𝑎 = ∅ → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) )
13 12 oveq2d ⊢ ( 𝑎 = ∅ → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) ) )
14 sumeq1 ⊢ ( 𝑎 = ∅ → Σ 𝑖 ∈ 𝑎 𝐵 = Σ 𝑖 ∈ ∅ 𝐵 )
15 14 mpteq2dv ⊢ ( 𝑎 = ∅ → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐵 ) )
16 13 15 eqeq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐵 ) ) )
17 10 16 imbi12d ⊢ ( 𝑎 = ∅ → ( ( 𝑎 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ) ↔ ( ∅ ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐵 ) ) ) )
18 17 imbi2d ⊢ ( 𝑎 = ∅ → ( ( 𝜑 → ( 𝑎 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐵 ) ) ) ) )
19 sseq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ⊆ 𝐼 ↔ 𝑏 ⊆ 𝐼 ) )
20 sumeq1 ⊢ ( 𝑎 = 𝑏 → Σ 𝑖 ∈ 𝑎 𝐴 = Σ 𝑖 ∈ 𝑏 𝐴 )
21 20 mpteq2dv ⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) )
22 21 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) )
23 sumeq1 ⊢ ( 𝑎 = 𝑏 → Σ 𝑖 ∈ 𝑎 𝐵 = Σ 𝑖 ∈ 𝑏 𝐵 )
24 23 mpteq2dv ⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) )
25 22 24 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) )
26 19 25 imbi12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ) ↔ ( 𝑏 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) )
27 26 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝜑 → ( 𝑎 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ) ) ↔ ( 𝜑 → ( 𝑏 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) ) )
28 sseq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑎 ⊆ 𝐼 ↔ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) )
29 sumeq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → Σ 𝑖 ∈ 𝑎 𝐴 = Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 )
30 29 mpteq2dv ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) )
31 30 oveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) )
32 sumeq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → Σ 𝑖 ∈ 𝑎 𝐵 = Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 )
33 32 mpteq2dv ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) )
34 31 33 eqeq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) )
35 28 34 imbi12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑎 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ) ↔ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) ) )
36 35 imbi2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝜑 → ( 𝑎 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ) ) ↔ ( 𝜑 → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) ) ) )
37 sseq1 ⊢ ( 𝑎 = 𝐼 → ( 𝑎 ⊆ 𝐼 ↔ 𝐼 ⊆ 𝐼 ) )
38 sumeq1 ⊢ ( 𝑎 = 𝐼 → Σ 𝑖 ∈ 𝑎 𝐴 = Σ 𝑖 ∈ 𝐼 𝐴 )
39 38 mpteq2dv ⊢ ( 𝑎 = 𝐼 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) )
40 39 oveq2d ⊢ ( 𝑎 = 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) ) )
41 sumeq1 ⊢ ( 𝑎 = 𝐼 → Σ 𝑖 ∈ 𝑎 𝐵 = Σ 𝑖 ∈ 𝐼 𝐵 )
42 41 mpteq2dv ⊢ ( 𝑎 = 𝐼 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐵 ) )
43 40 42 eqeq12d ⊢ ( 𝑎 = 𝐼 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐵 ) ) )
44 37 43 imbi12d ⊢ ( 𝑎 = 𝐼 → ( ( 𝑎 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ) ↔ ( 𝐼 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐵 ) ) ) )
45 44 imbi2d ⊢ ( 𝑎 = 𝐼 → ( ( 𝜑 → ( 𝑎 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑎 𝐵 ) ) ) ↔ ( 𝜑 → ( 𝐼 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐵 ) ) ) ) )
46 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 0 ∈ ℂ )
47 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
48 3 47 dvmptc ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑆 ↦ 0 ) ) = ( 𝑥 ∈ 𝑆 ↦ 0 ) )
49 2 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
50 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
51 3 50 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
52 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
53 49 51 52 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
54 1 53 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑆 ) )
55 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑆 ) ∧ 𝑋 ∈ 𝐽 ) → 𝑋 ⊆ 𝑆 )
56 54 4 55 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
57 3 46 46 48 56 1 2 4 dvmptres ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
58 sum0 ⊢ Σ 𝑖 ∈ ∅ 𝐴 = 0
59 58 mpteq2i ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 0 )
60 59 oveq2i ⊢ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) )
61 sum0 ⊢ Σ 𝑖 ∈ ∅ 𝐵 = 0
62 61 mpteq2i ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 0 )
63 57 60 62 3eqtr4g ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐵 ) )
64 63 a1d ⊢ ( 𝜑 → ( ∅ ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ∅ 𝐵 ) ) )
65 ssun1 ⊢ 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } )
66 sstr ⊢ ( ( 𝑏 ⊆ ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → 𝑏 ⊆ 𝐼 )
67 65 66 mpan ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → 𝑏 ⊆ 𝐼 )
68 67 imim1i ⊢ ( ( 𝑏 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) )
69 simpll ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → 𝜑 )
70 69 3 syl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → 𝑆 ∈ { ℝ , ℂ } )
71 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → 𝐼 ∈ Fin )
72 67 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑏 ⊆ 𝐼 )
73 71 72 ssfid ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑏 ∈ Fin )
74 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ 𝑏 ) → 𝜑 )
75 72 sselda ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ 𝑏 ) → 𝑖 ∈ 𝐼 )
76 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ 𝑏 ) → 𝑎 ∈ 𝑋 )
77 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 )
78 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐴
79 78 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ
80 77 79 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
81 eleq1w ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ∈ 𝑋 ↔ 𝑎 ∈ 𝑋 ) )
82 81 3anbi3d ⊢ ( 𝑥 = 𝑎 → ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) ) )
83 csbeq1a ⊢ ( 𝑥 = 𝑎 → 𝐴 = ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
84 83 eleq1d ⊢ ( 𝑥 = 𝑎 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
85 82 84 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ ) ) )
86 80 85 6 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
87 74 75 76 86 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ 𝑏 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
88 73 87 fsumcl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
89 88 adantlrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
90 sumex ⊢ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ V
91 90 a1i ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ V )
92 nfcv ⊢ Ⅎ 𝑎 Σ 𝑖 ∈ 𝑏 𝐴
93 nfcv ⊢ Ⅎ 𝑥 𝑏
94 93 78 nfsum ⊢ Ⅎ 𝑥 Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴
95 83 sumeq2sdv ⊢ ( 𝑥 = 𝑎 → Σ 𝑖 ∈ 𝑏 𝐴 = Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
96 92 94 95 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
97 96 oveq2i ⊢ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) )
98 nfcv ⊢ Ⅎ 𝑎 Σ 𝑖 ∈ 𝑏 𝐵
99 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐵
100 93 99 nfsum ⊢ Ⅎ 𝑥 Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵
101 csbeq1a ⊢ ( 𝑥 = 𝑎 → 𝐵 = ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
102 101 sumeq2sdv ⊢ ( 𝑥 = 𝑎 → Σ 𝑖 ∈ 𝑏 𝐵 = Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
103 98 100 102 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) = ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
104 97 103 eqeq12i ⊢ ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ↔ ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
105 104 biimpi ⊢ ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) → ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
106 105 ad2antll ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
107 simplll ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → 𝜑 )
108 ssun2 ⊢ { 𝑐 } ⊆ ( 𝑏 ∪ { 𝑐 } )
109 sstr ⊢ ( ( { 𝑐 } ⊆ ( 𝑏 ∪ { 𝑐 } ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → { 𝑐 } ⊆ 𝐼 )
110 108 109 mpan ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → { 𝑐 } ⊆ 𝐼 )
111 vex ⊢ 𝑐 ∈ V
112 111 snss ⊢ ( 𝑐 ∈ 𝐼 ↔ { 𝑐 } ⊆ 𝐼 )
113 110 112 sylibr ⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → 𝑐 ∈ 𝐼 )
114 113 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑐 ∈ 𝐼 )
115 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑎 ∈ 𝑋 )
116 6 3expb ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐴 ∈ ℂ )
117 116 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑖 ∈ 𝐼 ) ) → 𝐴 ∈ ℂ )
118 117 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑖 ∈ 𝐼 𝐴 ∈ ℂ )
119 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴
120 119 nfel1 ⊢ Ⅎ 𝑖 ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ
121 csbeq1a ⊢ ( 𝑖 = 𝑐 → ⦋ 𝑎 / 𝑥 ⦌ 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
122 121 eleq1d ⊢ ( 𝑖 = 𝑐 → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ ↔ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
123 79 120 84 122 rspc2 ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑖 ∈ 𝐼 𝐴 ∈ ℂ → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
124 123 ancoms ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑖 ∈ 𝐼 𝐴 ∈ ℂ → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
125 118 124 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) ) → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
126 107 114 115 125 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
127 126 adantlrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
128 7 3expb ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐵 ∈ ℂ )
129 128 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑖 ∈ 𝐼 ) ) → 𝐵 ∈ ℂ )
130 129 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑖 ∈ 𝐼 𝐵 ∈ ℂ )
131 99 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ
132 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵
133 132 nfel1 ⊢ Ⅎ 𝑖 ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ
134 101 eleq1d ⊢ ( 𝑥 = 𝑎 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
135 csbeq1a ⊢ ( 𝑖 = 𝑐 → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 = ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
136 135 eleq1d ⊢ ( 𝑖 = 𝑐 → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ ↔ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
137 131 133 134 136 rspc2 ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑖 ∈ 𝐼 𝐵 ∈ ℂ → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
138 137 ancoms ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑖 ∈ 𝐼 𝐵 ∈ ℂ → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
139 130 138 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) ) → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ )
140 107 114 115 139 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ )
141 140 adantlrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ )
142 113 ad2antrl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → 𝑐 ∈ 𝐼 )
143 nfv ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑐 ∈ 𝐼 )
144 nfcv ⊢ Ⅎ 𝑖 𝑆
145 nfcv ⊢ Ⅎ 𝑖 D
146 nfcv ⊢ Ⅎ 𝑖 𝑋
147 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑐 / 𝑖 ⦌ 𝐴
148 146 147 nfmpt ⊢ Ⅎ 𝑖 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 )
149 144 145 148 nfov ⊢ Ⅎ 𝑖 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) )
150 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑐 / 𝑖 ⦌ 𝐵
151 146 150 nfmpt ⊢ Ⅎ 𝑖 ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐵 )
152 149 151 nfeq ⊢ Ⅎ 𝑖 ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐵 )
153 143 152 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐵 ) )
154 eleq1w ⊢ ( 𝑖 = 𝑐 → ( 𝑖 ∈ 𝐼 ↔ 𝑐 ∈ 𝐼 ) )
155 154 anbi2d ⊢ ( 𝑖 = 𝑐 → ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ↔ ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ) )
156 csbeq1a ⊢ ( 𝑖 = 𝑐 → 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ 𝐴 )
157 156 mpteq2dv ⊢ ( 𝑖 = 𝑐 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) )
158 157 oveq2d ⊢ ( 𝑖 = 𝑐 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) )
159 csbeq1a ⊢ ( 𝑖 = 𝑐 → 𝐵 = ⦋ 𝑐 / 𝑖 ⦌ 𝐵 )
160 159 mpteq2dv ⊢ ( 𝑖 = 𝑐 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐵 ) )
161 158 160 eqeq12d ⊢ ( 𝑖 = 𝑐 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↔ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐵 ) ) )
162 155 161 imbi12d ⊢ ( 𝑖 = 𝑐 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) ↔ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐵 ) ) ) )
163 153 162 8 chvarfv ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐵 ) )
164 nfcv ⊢ Ⅎ 𝑎 ⦋ 𝑐 / 𝑖 ⦌ 𝐴
165 nfcv ⊢ Ⅎ 𝑥 𝑐
166 165 78 nfcsbw ⊢ Ⅎ 𝑥 ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴
167 83 csbeq2dv ⊢ ( 𝑥 = 𝑎 → ⦋ 𝑐 / 𝑖 ⦌ 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
168 164 166 167 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
169 168 oveq2i ⊢ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐴 ) ) = ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) )
170 nfcv ⊢ Ⅎ 𝑎 ⦋ 𝑐 / 𝑖 ⦌ 𝐵
171 165 99 nfcsbw ⊢ Ⅎ 𝑥 ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵
172 101 csbeq2dv ⊢ ( 𝑥 = 𝑎 → ⦋ 𝑐 / 𝑖 ⦌ 𝐵 = ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
173 170 171 172 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ 𝐵 ) = ( 𝑎 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
174 163 169 173 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑎 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
175 69 142 174 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑎 ∈ 𝑋 ↦ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
176 70 89 91 106 127 141 175 dvmptadd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) ) = ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) ) )
177 nfcv ⊢ Ⅎ 𝑎 Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴
178 nfcv ⊢ Ⅎ 𝑥 ( 𝑏 ∪ { 𝑐 } )
179 178 78 nfsum ⊢ Ⅎ 𝑥 Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐴
180 83 sumeq2sdv ⊢ ( 𝑥 = 𝑎 → Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 = Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
181 177 179 180 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
182 simpllr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ¬ 𝑐 ∈ 𝑏 )
183 disjsn ⊢ ( ( 𝑏 ∩ { 𝑐 } ) = ∅ ↔ ¬ 𝑐 ∈ 𝑏 )
184 182 183 sylibr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑏 ∩ { 𝑐 } ) = ∅ )
185 eqidd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑏 ∪ { 𝑐 } ) = ( 𝑏 ∪ { 𝑐 } ) )
186 simplr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 )
187 71 186 ssfid ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑏 ∪ { 𝑐 } ) ∈ Fin )
188 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → 𝜑 )
189 186 sselda ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → 𝑖 ∈ 𝐼 )
190 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → 𝑎 ∈ 𝑋 )
191 188 189 190 86 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ )
192 184 185 187 191 fsumsplit ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐴 = ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + Σ 𝑖 ∈ { 𝑐 } ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) )
193 sumsns ⊢ ( ( 𝑐 ∈ V ∧ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ∈ ℂ ) → Σ 𝑖 ∈ { 𝑐 } ⦋ 𝑎 / 𝑥 ⦌ 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
194 111 126 193 sylancr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ { 𝑐 } ⦋ 𝑎 / 𝑥 ⦌ 𝐴 = ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 )
195 194 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + Σ 𝑖 ∈ { 𝑐 } ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) = ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) )
196 192 195 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐴 = ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) )
197 196 mpteq2dva ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) )
198 181 197 syl5eq ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) )
199 198 adantrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) = ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) )
200 199 oveq2d ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑆 D ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐴 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐴 ) ) ) )
201 nfcv ⊢ Ⅎ 𝑎 Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵
202 178 99 nfsum ⊢ Ⅎ 𝑥 Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐵
203 101 sumeq2sdv ⊢ ( 𝑥 = 𝑎 → Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 = Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
204 201 202 203 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) = ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
205 77 131 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ )
206 82 134 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ ) ) )
207 205 206 7 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ 𝑋 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ )
208 188 189 190 207 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ )
209 184 185 187 208 fsumsplit ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐵 = ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 + Σ 𝑖 ∈ { 𝑐 } ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
210 sumsns ⊢ ( ( 𝑐 ∈ V ∧ ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ ℂ ) → Σ 𝑖 ∈ { 𝑐 } ⦋ 𝑎 / 𝑥 ⦌ 𝐵 = ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
211 111 140 210 sylancr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ { 𝑐 } ⦋ 𝑎 / 𝑥 ⦌ 𝐵 = ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
212 211 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 + Σ 𝑖 ∈ { 𝑐 } ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) = ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
213 209 212 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) ∧ 𝑎 ∈ 𝑋 ) → Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐵 = ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
214 213 mpteq2dva ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑎 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) = ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) ) )
215 204 214 syl5eq ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) = ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) ) )
216 215 adantrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) = ( 𝑎 ∈ 𝑋 ↦ ( Σ 𝑖 ∈ 𝑏 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) ) )
217 176 200 216 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) ∧ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 ∧ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) )
218 217 exp32 ⊢ ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) ) )
219 218 a2d ⊢ ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) → ( ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) ) )
220 68 219 syl5 ⊢ ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑏 ) → ( ( 𝑏 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) ) )
221 220 expcom ⊢ ( ¬ 𝑐 ∈ 𝑏 → ( 𝜑 → ( ( 𝑏 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) ) ) )
222 221 adantl ⊢ ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) → ( 𝜑 → ( ( 𝑏 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) ) ) )
223 222 a2d ⊢ ( ( 𝑏 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑏 ) → ( ( 𝜑 → ( 𝑏 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝑏 𝐵 ) ) ) → ( 𝜑 → ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐵 ) ) ) ) )
224 18 27 36 45 64 223 findcard2s ⊢ ( 𝐼 ∈ Fin → ( 𝜑 → ( 𝐼 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐵 ) ) ) )
225 5 224 mpcom ⊢ ( 𝜑 → ( 𝐼 ⊆ 𝐼 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐵 ) ) )
226 9 225 mpi ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑖 ∈ 𝐼 𝐵 ) )