This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsumrlim

Description: Limit of a finite sum of converging sequences. Note that C ( k ) is a collection of functions with implicit parameter k , each of which converges to D ( k ) as n ~> +oo . (Contributed by Mario Carneiro, 22-May-2016)

Ref Expression
Hypotheses fsumrlim.1 
|- ( ph -> A C_ RR )
fsumrlim.2 
|- ( ph -> B e. Fin )
fsumrlim.3 
|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )
fsumrlim.4 
|- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) ~~>r D )
Assertion fsumrlim 
|- ( ph -> ( x e. A |-> sum_ k e. B C ) ~~>r sum_ k e. B D )

Proof

Step Hyp Ref Expression
1 fsumrlim.1 
 |-  ( ph -> A C_ RR )
2 fsumrlim.2 
 |-  ( ph -> B e. Fin )
3 fsumrlim.3 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )
4 fsumrlim.4 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> C ) ~~>r D )
5 ssid 
 |-  B C_ B
6 sseq1 
 |-  ( w = (/) -> ( w C_ B <-> (/) C_ B ) )
7 sumeq1 
 |-  ( w = (/) -> sum_ k e. w C = sum_ k e. (/) C )
8 sum0 
 |-  sum_ k e. (/) C = 0
9 7 8 eqtrdi 
 |-  ( w = (/) -> sum_ k e. w C = 0 )
10 9 mpteq2dv 
 |-  ( w = (/) -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> 0 ) )
11 sumeq1 
 |-  ( w = (/) -> sum_ k e. w D = sum_ k e. (/) D )
12 sum0 
 |-  sum_ k e. (/) D = 0
13 11 12 eqtrdi 
 |-  ( w = (/) -> sum_ k e. w D = 0 )
14 10 13 breq12d 
 |-  ( w = (/) -> ( ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D <-> ( x e. A |-> 0 ) ~~>r 0 ) )
15 6 14 imbi12d 
 |-  ( w = (/) -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D ) <-> ( (/) C_ B -> ( x e. A |-> 0 ) ~~>r 0 ) ) )
16 15 imbi2d 
 |-  ( w = (/) -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D ) ) <-> ( ph -> ( (/) C_ B -> ( x e. A |-> 0 ) ~~>r 0 ) ) ) )
17 sseq1 
 |-  ( w = y -> ( w C_ B <-> y C_ B ) )
18 sumeq1 
 |-  ( w = y -> sum_ k e. w C = sum_ k e. y C )
19 18 mpteq2dv 
 |-  ( w = y -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. y C ) )
20 sumeq1 
 |-  ( w = y -> sum_ k e. w D = sum_ k e. y D )
21 19 20 breq12d 
 |-  ( w = y -> ( ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D <-> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) )
22 17 21 imbi12d 
 |-  ( w = y -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D ) <-> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) ) )
23 22 imbi2d 
 |-  ( w = y -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D ) ) <-> ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) ) ) )
24 sseq1 
 |-  ( w = ( y u. { z } ) -> ( w C_ B <-> ( y u. { z } ) C_ B ) )
25 sumeq1 
 |-  ( w = ( y u. { z } ) -> sum_ k e. w C = sum_ k e. ( y u. { z } ) C )
26 25 mpteq2dv 
 |-  ( w = ( y u. { z } ) -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. ( y u. { z } ) C ) )
27 sumeq1 
 |-  ( w = ( y u. { z } ) -> sum_ k e. w D = sum_ k e. ( y u. { z } ) D )
28 26 27 breq12d 
 |-  ( w = ( y u. { z } ) -> ( ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D <-> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) )
29 24 28 imbi12d 
 |-  ( w = ( y u. { z } ) -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D ) <-> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) ) )
30 29 imbi2d 
 |-  ( w = ( y u. { z } ) -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D ) ) <-> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) ) ) )
31 sseq1 
 |-  ( w = B -> ( w C_ B <-> B C_ B ) )
32 sumeq1 
 |-  ( w = B -> sum_ k e. w C = sum_ k e. B C )
33 32 mpteq2dv 
 |-  ( w = B -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. B C ) )
34 sumeq1 
 |-  ( w = B -> sum_ k e. w D = sum_ k e. B D )
35 33 34 breq12d 
 |-  ( w = B -> ( ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D <-> ( x e. A |-> sum_ k e. B C ) ~~>r sum_ k e. B D ) )
36 31 35 imbi12d 
 |-  ( w = B -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D ) <-> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) ~~>r sum_ k e. B D ) ) )
37 36 imbi2d 
 |-  ( w = B -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~>r sum_ k e. w D ) ) <-> ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) ~~>r sum_ k e. B D ) ) ) )
38 0cn 
 |-  0 e. CC
39 rlimconst 
 |-  ( ( A C_ RR /\ 0 e. CC ) -> ( x e. A |-> 0 ) ~~>r 0 )
40 1 38 39 sylancl 
 |-  ( ph -> ( x e. A |-> 0 ) ~~>r 0 )
41 40 a1d 
 |-  ( ph -> ( (/) C_ B -> ( x e. A |-> 0 ) ~~>r 0 ) )
42 ssun1 
 |-  y C_ ( y u. { z } )
43 sstr 
 |-  ( ( y C_ ( y u. { z } ) /\ ( y u. { z } ) C_ B ) -> y C_ B )
44 42 43 mpan 
 |-  ( ( y u. { z } ) C_ B -> y C_ B )
45 44 imim1i 
 |-  ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) )
46 sumex 
 |-  sum_ k e. y [_ w / x ]_ C e. _V
47 46 a1i 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) /\ w e. A ) -> sum_ k e. y [_ w / x ]_ C e. _V )
48 simprr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y u. { z } ) C_ B )
49 48 unssbd 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> { z } C_ B )
50 vex 
 |-  z e. _V
51 50 snss 
 |-  ( z e. B <-> { z } C_ B )
52 49 51 sylibr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> z e. B )
53 52 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> z e. B )
54 3 anass1rs 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> C e. V )
55 54 4 rlimmptrcl 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> C e. CC )
56 55 an32s 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. CC )
57 56 adantllr 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. B ) -> C e. CC )
58 57 ralrimiva 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> A. k e. B C e. CC )
59 nfcsb1v 
 |-  F/_ k [_ z / k ]_ C
60 59 nfel1 
 |-  F/ k [_ z / k ]_ C e. CC
61 csbeq1a 
 |-  ( k = z -> C = [_ z / k ]_ C )
62 61 eleq1d 
 |-  ( k = z -> ( C e. CC <-> [_ z / k ]_ C e. CC ) )
63 60 62 rspc 
 |-  ( z e. B -> ( A. k e. B C e. CC -> [_ z / k ]_ C e. CC ) )
64 53 58 63 sylc 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> [_ z / k ]_ C e. CC )
65 64 ralrimiva 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A. x e. A [_ z / k ]_ C e. CC )
66 65 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> A. x e. A [_ z / k ]_ C e. CC )
67 nfcsb1v 
 |-  F/_ x [_ w / x ]_ [_ z / k ]_ C
68 67 nfel1 
 |-  F/ x [_ w / x ]_ [_ z / k ]_ C e. CC
69 csbeq1a 
 |-  ( x = w -> [_ z / k ]_ C = [_ w / x ]_ [_ z / k ]_ C )
70 69 eleq1d 
 |-  ( x = w -> ( [_ z / k ]_ C e. CC <-> [_ w / x ]_ [_ z / k ]_ C e. CC ) )
71 68 70 rspc 
 |-  ( w e. A -> ( A. x e. A [_ z / k ]_ C e. CC -> [_ w / x ]_ [_ z / k ]_ C e. CC ) )
72 66 71 mpan9 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) /\ w e. A ) -> [_ w / x ]_ [_ z / k ]_ C e. CC )
73 72 elexd 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) /\ w e. A ) -> [_ w / x ]_ [_ z / k ]_ C e. _V )
74 nfcv 
 |-  F/_ w sum_ k e. y C
75 nfcv 
 |-  F/_ x y
76 nfcsb1v 
 |-  F/_ x [_ w / x ]_ C
77 75 76 nfsum 
 |-  F/_ x sum_ k e. y [_ w / x ]_ C
78 csbeq1a 
 |-  ( x = w -> C = [_ w / x ]_ C )
79 78 sumeq2sdv 
 |-  ( x = w -> sum_ k e. y C = sum_ k e. y [_ w / x ]_ C )
80 74 77 79 cbvmpt 
 |-  ( x e. A |-> sum_ k e. y C ) = ( w e. A |-> sum_ k e. y [_ w / x ]_ C )
81 simpr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D )
82 80 81 eqbrtrrid 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( w e. A |-> sum_ k e. y [_ w / x ]_ C ) ~~>r sum_ k e. y D )
83 nfcv 
 |-  F/_ w [_ z / k ]_ C
84 83 67 69 cbvmpt 
 |-  ( x e. A |-> [_ z / k ]_ C ) = ( w e. A |-> [_ w / x ]_ [_ z / k ]_ C )
85 4 ralrimiva 
 |-  ( ph -> A. k e. B ( x e. A |-> C ) ~~>r D )
86 85 adantr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A. k e. B ( x e. A |-> C ) ~~>r D )
87 nfcv 
 |-  F/_ k A
88 87 59 nfmpt 
 |-  F/_ k ( x e. A |-> [_ z / k ]_ C )
89 nfcv 
 |-  F/_ k ~~>r
90 nfcsb1v 
 |-  F/_ k [_ z / k ]_ D
91 88 89 90 nfbr 
 |-  F/ k ( x e. A |-> [_ z / k ]_ C ) ~~>r [_ z / k ]_ D
92 61 mpteq2dv 
 |-  ( k = z -> ( x e. A |-> C ) = ( x e. A |-> [_ z / k ]_ C ) )
93 csbeq1a 
 |-  ( k = z -> D = [_ z / k ]_ D )
94 92 93 breq12d 
 |-  ( k = z -> ( ( x e. A |-> C ) ~~>r D <-> ( x e. A |-> [_ z / k ]_ C ) ~~>r [_ z / k ]_ D ) )
95 91 94 rspc 
 |-  ( z e. B -> ( A. k e. B ( x e. A |-> C ) ~~>r D -> ( x e. A |-> [_ z / k ]_ C ) ~~>r [_ z / k ]_ D ) )
96 52 86 95 sylc 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> [_ z / k ]_ C ) ~~>r [_ z / k ]_ D )
97 96 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( x e. A |-> [_ z / k ]_ C ) ~~>r [_ z / k ]_ D )
98 84 97 eqbrtrrid 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( w e. A |-> [_ w / x ]_ [_ z / k ]_ C ) ~~>r [_ z / k ]_ D )
99 47 73 82 98 rlimadd 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( w e. A |-> ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C ) ) ~~>r ( sum_ k e. y D + [_ z / k ]_ D ) )
100 simprl 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> -. z e. y )
101 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
102 100 101 sylibr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y i^i { z } ) = (/) )
103 102 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y i^i { z } ) = (/) )
104 eqidd 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y u. { z } ) = ( y u. { z } ) )
105 2 adantr 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> B e. Fin )
106 105 48 ssfid 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y u. { z } ) e. Fin )
107 106 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y u. { z } ) e. Fin )
108 48 sselda 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ k e. ( y u. { z } ) ) -> k e. B )
109 108 adantlr 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. ( y u. { z } ) ) -> k e. B )
110 109 57 syldan 
 |-  ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. ( y u. { z } ) ) -> C e. CC )
111 103 104 107 110 fsumsplit 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. ( y u. { z } ) C = ( sum_ k e. y C + sum_ k e. { z } C ) )
112 csbeq1a 
 |-  ( k = w -> C = [_ w / k ]_ C )
113 nfcv 
 |-  F/_ w C
114 nfcsb1v 
 |-  F/_ k [_ w / k ]_ C
115 112 113 114 cbvsum 
 |-  sum_ k e. { z } C = sum_ w e. { z } [_ w / k ]_ C
116 csbeq1 
 |-  ( w = z -> [_ w / k ]_ C = [_ z / k ]_ C )
117 116 sumsn 
 |-  ( ( z e. B /\ [_ z / k ]_ C e. CC ) -> sum_ w e. { z } [_ w / k ]_ C = [_ z / k ]_ C )
118 53 64 117 syl2anc 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ w e. { z } [_ w / k ]_ C = [_ z / k ]_ C )
119 115 118 eqtrid 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. { z } C = [_ z / k ]_ C )
120 119 oveq2d 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( sum_ k e. y C + sum_ k e. { z } C ) = ( sum_ k e. y C + [_ z / k ]_ C ) )
121 111 120 eqtrd 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. ( y u. { z } ) C = ( sum_ k e. y C + [_ z / k ]_ C ) )
122 121 mpteq2dva 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( x e. A |-> ( sum_ k e. y C + [_ z / k ]_ C ) ) )
123 122 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( x e. A |-> ( sum_ k e. y C + [_ z / k ]_ C ) ) )
124 nfcv 
 |-  F/_ w ( sum_ k e. y C + [_ z / k ]_ C )
125 nfcv 
 |-  F/_ x +
126 77 125 67 nfov 
 |-  F/_ x ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C )
127 79 69 oveq12d 
 |-  ( x = w -> ( sum_ k e. y C + [_ z / k ]_ C ) = ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C ) )
128 124 126 127 cbvmpt 
 |-  ( x e. A |-> ( sum_ k e. y C + [_ z / k ]_ C ) ) = ( w e. A |-> ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C ) )
129 123 128 eqtrdi 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( w e. A |-> ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C ) ) )
130 eqidd 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y u. { z } ) = ( y u. { z } ) )
131 rlimcl 
 |-  ( ( x e. A |-> C ) ~~>r D -> D e. CC )
132 4 131 syl 
 |-  ( ( ph /\ k e. B ) -> D e. CC )
133 132 adantlr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ k e. B ) -> D e. CC )
134 108 133 syldan 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ k e. ( y u. { z } ) ) -> D e. CC )
135 102 130 106 134 fsumsplit 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> sum_ k e. ( y u. { z } ) D = ( sum_ k e. y D + sum_ k e. { z } D ) )
136 csbeq1a 
 |-  ( k = w -> D = [_ w / k ]_ D )
137 nfcv 
 |-  F/_ w D
138 nfcsb1v 
 |-  F/_ k [_ w / k ]_ D
139 136 137 138 cbvsum 
 |-  sum_ k e. { z } D = sum_ w e. { z } [_ w / k ]_ D
140 133 ralrimiva 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A. k e. B D e. CC )
141 90 nfel1 
 |-  F/ k [_ z / k ]_ D e. CC
142 93 eleq1d 
 |-  ( k = z -> ( D e. CC <-> [_ z / k ]_ D e. CC ) )
143 141 142 rspc 
 |-  ( z e. B -> ( A. k e. B D e. CC -> [_ z / k ]_ D e. CC ) )
144 52 140 143 sylc 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> [_ z / k ]_ D e. CC )
145 csbeq1 
 |-  ( w = z -> [_ w / k ]_ D = [_ z / k ]_ D )
146 145 sumsn 
 |-  ( ( z e. B /\ [_ z / k ]_ D e. CC ) -> sum_ w e. { z } [_ w / k ]_ D = [_ z / k ]_ D )
147 52 144 146 syl2anc 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> sum_ w e. { z } [_ w / k ]_ D = [_ z / k ]_ D )
148 139 147 eqtrid 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> sum_ k e. { z } D = [_ z / k ]_ D )
149 148 oveq2d 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( sum_ k e. y D + sum_ k e. { z } D ) = ( sum_ k e. y D + [_ z / k ]_ D ) )
150 135 149 eqtrd 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> sum_ k e. ( y u. { z } ) D = ( sum_ k e. y D + [_ z / k ]_ D ) )
151 150 adantr 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> sum_ k e. ( y u. { z } ) D = ( sum_ k e. y D + [_ z / k ]_ D ) )
152 99 129 151 3brtr4d 
 |-  ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D )
153 152 ex 
 |-  ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) )
154 153 expr 
 |-  ( ( ph /\ -. z e. y ) -> ( ( y u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) ) )
155 154 a2d 
 |-  ( ( ph /\ -. z e. y ) -> ( ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) ) )
156 45 155 syl5 
 |-  ( ( ph /\ -. z e. y ) -> ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) ) )
157 156 expcom 
 |-  ( -. z e. y -> ( ph -> ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) ) ) )
158 157 a2d 
 |-  ( -. z e. y -> ( ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) ) -> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) ) ) )
159 158 adantl 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~>r sum_ k e. y D ) ) -> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~>r sum_ k e. ( y u. { z } ) D ) ) ) )
160 16 23 30 37 41 159 findcard2s 
 |-  ( B e. Fin -> ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) ~~>r sum_ k e. B D ) ) )
161 2 160 mpcom 
 |-  ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) ~~>r sum_ k e. B D ) )
162 5 161 mpi 
 |-  ( ph -> ( x e. A |-> sum_ k e. B C ) ~~>r sum_ k e. B D )