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 ) |