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 nfcv
 |-  F/_ w C
113 nfcsb1v
 |-  F/_ k [_ w / k ]_ C
114 csbeq1a
 |-  ( k = w -> C = [_ w / k ]_ C )
115 112 113 114 cbvsumi
 |-  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 nfcv
 |-  F/_ w D
137 nfcsb1v
 |-  F/_ k [_ w / k ]_ D
138 csbeq1a
 |-  ( k = w -> D = [_ w / k ]_ D )
139 136 137 138 cbvsumi
 |-  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 )