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 eqtrid ⊒ ( ( ( πœ‘ ∧ Β¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 βˆͺ { 𝑐 } ) βŠ† 𝐼 ) β†’ ( π‘₯ ∈ 𝑋 ↦ Ξ£ 𝑖 ∈ ( 𝑏 βˆͺ { 𝑐 } ) 𝐴 ) = ( π‘Ž ∈ 𝑋 ↦ ( Ξ£ 𝑖 ∈ 𝑏 ⦋ π‘Ž / π‘₯ ⦌ 𝐴 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ π‘Ž / π‘₯ ⦌ 𝐴 ) ) )
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 eqtrid ⊒ ( ( ( πœ‘ ∧ Β¬ 𝑐 ∈ 𝑏 ) ∧ ( 𝑏 βˆͺ { 𝑐 } ) βŠ† 𝐼 ) β†’ ( π‘₯ ∈ 𝑋 ↦ Ξ£ 𝑖 ∈ ( 𝑏 βˆͺ { 𝑐 } ) 𝐡 ) = ( π‘Ž ∈ 𝑋 ↦ ( Ξ£ 𝑖 ∈ 𝑏 ⦋ π‘Ž / π‘₯ ⦌ 𝐡 + ⦋ 𝑐 / 𝑖 ⦌ ⦋ π‘Ž / π‘₯ ⦌ 𝐡 ) ) )
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 ( π‘₯ ∈ 𝑋 ↦ Ξ£ 𝑖 ∈ 𝐼 𝐴 ) ) = ( π‘₯ ∈ 𝑋 ↦ Ξ£ 𝑖 ∈ 𝐼 𝐡 ) )