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 
|- J = ( K |`t S )
dvmptfsum.k 
|- K = ( TopOpen ` CCfld )
dvmptfsum.s 
|- ( ph -> S e. { RR , CC } )
dvmptfsum.x 
|- ( ph -> X e. J )
dvmptfsum.i 
|- ( ph -> I e. Fin )
dvmptfsum.a 
|- ( ( ph /\ i e. I /\ x e. X ) -> A e. CC )
dvmptfsum.b 
|- ( ( ph /\ i e. I /\ x e. X ) -> B e. CC )
dvmptfsum.d 
|- ( ( ph /\ i e. I ) -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
Assertion dvmptfsum 
|- ( ph -> ( S _D ( x e. X |-> sum_ i e. I A ) ) = ( x e. X |-> sum_ i e. I B ) )

Proof

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