Metamath Proof Explorer

Theorem itgfsum

Description: Take a finite sum of integrals over the same domain. (Contributed by Mario Carneiro, 24-Aug-2014)

Ref Expression
Hypotheses itgfsum.1 
|- ( ph -> A e. dom vol )
itgfsum.2 
|- ( ph -> B e. Fin )
itgfsum.3 
|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )
itgfsum.4 
|- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. L^1 )
Assertion itgfsum 
|- ( ph -> ( ( x e. A |-> sum_ k e. B C ) e. L^1 /\ S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) )

Proof

Step Hyp Ref Expression
1 itgfsum.1 
 |-  ( ph -> A e. dom vol )
2 itgfsum.2 
 |-  ( ph -> B e. Fin )
3 itgfsum.3 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )
4 itgfsum.4 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. L^1 )
5 ssid 
 |-  B C_ B
6 sseq1 
 |-  ( t = (/) -> ( t C_ B <-> (/) C_ B ) )
7 itgz 
 |-  S. A 0 _d x = 0
8 sumeq1 
 |-  ( t = (/) -> sum_ k e. t C = sum_ k e. (/) C )
9 sum0 
 |-  sum_ k e. (/) C = 0
10 8 9 eqtrdi 
 |-  ( t = (/) -> sum_ k e. t C = 0 )
11 10 adantr 
 |-  ( ( t = (/) /\ x e. A ) -> sum_ k e. t C = 0 )
12 11 itgeq2dv 
 |-  ( t = (/) -> S. A sum_ k e. t C _d x = S. A 0 _d x )
13 sumeq1 
 |-  ( t = (/) -> sum_ k e. t S. A C _d x = sum_ k e. (/) S. A C _d x )
14 sum0 
 |-  sum_ k e. (/) S. A C _d x = 0
15 13 14 eqtrdi 
 |-  ( t = (/) -> sum_ k e. t S. A C _d x = 0 )
16 7 12 15 3eqtr4a 
 |-  ( t = (/) -> S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x )
17 10 mpteq2dv 
 |-  ( t = (/) -> ( x e. A |-> sum_ k e. t C ) = ( x e. A |-> 0 ) )
18 fconstmpt 
 |-  ( A X. { 0 } ) = ( x e. A |-> 0 )
19 17 18 eqtr4di 
 |-  ( t = (/) -> ( x e. A |-> sum_ k e. t C ) = ( A X. { 0 } ) )
20 19 eleq1d 
 |-  ( t = (/) -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 <-> ( A X. { 0 } ) e. L^1 ) )
21 20 anbi1d 
 |-  ( t = (/) -> ( ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) <-> ( ( A X. { 0 } ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) )
22 16 21 mpbiran2d 
 |-  ( t = (/) -> ( ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) <-> ( A X. { 0 } ) e. L^1 ) )
23 6 22 imbi12d 
 |-  ( t = (/) -> ( ( t C_ B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) <-> ( (/) C_ B -> ( A X. { 0 } ) e. L^1 ) ) )
24 23 imbi2d 
 |-  ( t = (/) -> ( ( ph -> ( t C_ B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) ) <-> ( ph -> ( (/) C_ B -> ( A X. { 0 } ) e. L^1 ) ) ) )
25 sseq1 
 |-  ( t = w -> ( t C_ B <-> w C_ B ) )
26 sumeq1 
 |-  ( t = w -> sum_ k e. t C = sum_ k e. w C )
27 26 mpteq2dv 
 |-  ( t = w -> ( x e. A |-> sum_ k e. t C ) = ( x e. A |-> sum_ k e. w C ) )
28 27 eleq1d 
 |-  ( t = w -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 <-> ( x e. A |-> sum_ k e. w C ) e. L^1 ) )
29 26 adantr 
 |-  ( ( t = w /\ x e. A ) -> sum_ k e. t C = sum_ k e. w C )
30 29 itgeq2dv 
 |-  ( t = w -> S. A sum_ k e. t C _d x = S. A sum_ k e. w C _d x )
31 sumeq1 
 |-  ( t = w -> sum_ k e. t S. A C _d x = sum_ k e. w S. A C _d x )
32 30 31 eqeq12d 
 |-  ( t = w -> ( S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x <-> S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) )
33 28 32 anbi12d 
 |-  ( t = w -> ( ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) <-> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) )
34 25 33 imbi12d 
 |-  ( t = w -> ( ( t C_ B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) <-> ( w C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) ) )
35 34 imbi2d 
 |-  ( t = w -> ( ( ph -> ( t C_ B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) ) <-> ( ph -> ( w C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) ) ) )
36 sseq1 
 |-  ( t = ( w u. { z } ) -> ( t C_ B <-> ( w u. { z } ) C_ B ) )
37 sumeq1 
 |-  ( t = ( w u. { z } ) -> sum_ k e. t C = sum_ k e. ( w u. { z } ) C )
38 37 mpteq2dv 
 |-  ( t = ( w u. { z } ) -> ( x e. A |-> sum_ k e. t C ) = ( x e. A |-> sum_ k e. ( w u. { z } ) C ) )
39 38 eleq1d 
 |-  ( t = ( w u. { z } ) -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 <-> ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 ) )
40 37 adantr 
 |-  ( ( t = ( w u. { z } ) /\ x e. A ) -> sum_ k e. t C = sum_ k e. ( w u. { z } ) C )
41 40 itgeq2dv 
 |-  ( t = ( w u. { z } ) -> S. A sum_ k e. t C _d x = S. A sum_ k e. ( w u. { z } ) C _d x )
42 sumeq1 
 |-  ( t = ( w u. { z } ) -> sum_ k e. t S. A C _d x = sum_ k e. ( w u. { z } ) S. A C _d x )
43 41 42 eqeq12d 
 |-  ( t = ( w u. { z } ) -> ( S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x <-> S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) )
44 39 43 anbi12d 
 |-  ( t = ( w u. { z } ) -> ( ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) <-> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) )
45 36 44 imbi12d 
 |-  ( t = ( w u. { z } ) -> ( ( t C_ B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) <-> ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) ) )
46 45 imbi2d 
 |-  ( t = ( w u. { z } ) -> ( ( ph -> ( t C_ B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) ) <-> ( ph -> ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) ) ) )
47 sseq1 
 |-  ( t = B -> ( t C_ B <-> B C_ B ) )
48 sumeq1 
 |-  ( t = B -> sum_ k e. t C = sum_ k e. B C )
49 48 mpteq2dv 
 |-  ( t = B -> ( x e. A |-> sum_ k e. t C ) = ( x e. A |-> sum_ k e. B C ) )
50 49 eleq1d 
 |-  ( t = B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 <-> ( x e. A |-> sum_ k e. B C ) e. L^1 ) )
51 48 adantr 
 |-  ( ( t = B /\ x e. A ) -> sum_ k e. t C = sum_ k e. B C )
52 51 itgeq2dv 
 |-  ( t = B -> S. A sum_ k e. t C _d x = S. A sum_ k e. B C _d x )
53 sumeq1 
 |-  ( t = B -> sum_ k e. t S. A C _d x = sum_ k e. B S. A C _d x )
54 52 53 eqeq12d 
 |-  ( t = B -> ( S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x <-> S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) )
55 50 54 anbi12d 
 |-  ( t = B -> ( ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) <-> ( ( x e. A |-> sum_ k e. B C ) e. L^1 /\ S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) ) )
56 47 55 imbi12d 
 |-  ( t = B -> ( ( t C_ B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) <-> ( B C_ B -> ( ( x e. A |-> sum_ k e. B C ) e. L^1 /\ S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) ) ) )
57 56 imbi2d 
 |-  ( t = B -> ( ( ph -> ( t C_ B -> ( ( x e. A |-> sum_ k e. t C ) e. L^1 /\ S. A sum_ k e. t C _d x = sum_ k e. t S. A C _d x ) ) ) <-> ( ph -> ( B C_ B -> ( ( x e. A |-> sum_ k e. B C ) e. L^1 /\ S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) ) ) ) )
58 ibl0 
 |-  ( A e. dom vol -> ( A X. { 0 } ) e. L^1 )
59 1 58 syl 
 |-  ( ph -> ( A X. { 0 } ) e. L^1 )
60 59 a1d 
 |-  ( ph -> ( (/) C_ B -> ( A X. { 0 } ) e. L^1 ) )
61 ssun1 
 |-  w C_ ( w u. { z } )
62 sstr 
 |-  ( ( w C_ ( w u. { z } ) /\ ( w u. { z } ) C_ B ) -> w C_ B )
63 61 62 mpan 
 |-  ( ( w u. { z } ) C_ B -> w C_ B )
64 63 imim1i 
 |-  ( ( w C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) )
65 nfcv 
 |-  F/_ m C
66 nfcsb1v 
 |-  F/_ k [_ m / k ]_ C
67 csbeq1a 
 |-  ( k = m -> C = [_ m / k ]_ C )
68 65 66 67 cbvsumi 
 |-  sum_ k e. ( w u. { z } ) C = sum_ m e. ( w u. { z } ) [_ m / k ]_ C
69 simprl 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> -. z e. w )
70 disjsn 
 |-  ( ( w i^i { z } ) = (/) <-> -. z e. w )
71 69 70 sylibr 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( w i^i { z } ) = (/) )
72 71 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> ( w i^i { z } ) = (/) )
73 eqidd 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> ( w u. { z } ) = ( w u. { z } ) )
74 2 adantr 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> B e. Fin )
75 simprr 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( w u. { z } ) C_ B )
76 74 75 ssfid 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( w u. { z } ) e. Fin )
77 76 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> ( w u. { z } ) e. Fin )
78 simplrr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> ( w u. { z } ) C_ B )
79 78 sselda 
 |-  ( ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) /\ m e. ( w u. { z } ) ) -> m e. B )
80 iblmbf 
 |-  ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
81 4 80 syl 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. MblFn )
82 3 anass1rs 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> C e. V )
83 81 82 mbfmptcl 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> C e. CC )
84 83 an32s 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. CC )
85 84 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. k e. B C e. CC )
86 85 adantlr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> A. k e. B C e. CC )
87 65 nfel1 
 |-  F/ m C e. CC
88 66 nfel1 
 |-  F/ k [_ m / k ]_ C e. CC
89 67 eleq1d 
 |-  ( k = m -> ( C e. CC <-> [_ m / k ]_ C e. CC ) )
90 87 88 89 cbvralw 
 |-  ( A. k e. B C e. CC <-> A. m e. B [_ m / k ]_ C e. CC )
91 86 90 sylib 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> A. m e. B [_ m / k ]_ C e. CC )
92 91 r19.21bi 
 |-  ( ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) /\ m e. B ) -> [_ m / k ]_ C e. CC )
93 79 92 syldan 
 |-  ( ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) /\ m e. ( w u. { z } ) ) -> [_ m / k ]_ C e. CC )
94 72 73 77 93 fsumsplit 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ m e. ( w u. { z } ) [_ m / k ]_ C = ( sum_ m e. w [_ m / k ]_ C + sum_ m e. { z } [_ m / k ]_ C ) )
95 vex 
 |-  z e. _V
96 csbeq1 
 |-  ( m = z -> [_ m / k ]_ C = [_ z / k ]_ C )
97 96 eleq1d 
 |-  ( m = z -> ( [_ m / k ]_ C e. CC <-> [_ z / k ]_ C e. CC ) )
98 75 unssbd 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> { z } C_ B )
99 95 snss 
 |-  ( z e. B <-> { z } C_ B )
100 98 99 sylibr 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> z e. B )
101 100 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> z e. B )
102 97 91 101 rspcdva 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> [_ z / k ]_ C e. CC )
103 96 sumsn 
 |-  ( ( z e. _V /\ [_ z / k ]_ C e. CC ) -> sum_ m e. { z } [_ m / k ]_ C = [_ z / k ]_ C )
104 95 102 103 sylancr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ m e. { z } [_ m / k ]_ C = [_ z / k ]_ C )
105 104 oveq2d 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> ( sum_ m e. w [_ m / k ]_ C + sum_ m e. { z } [_ m / k ]_ C ) = ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) )
106 94 105 eqtrd 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ m e. ( w u. { z } ) [_ m / k ]_ C = ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) )
107 68 106 eqtrid 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. ( w u. { z } ) C = ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) )
108 107 mpteq2dva 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( x e. A |-> sum_ k e. ( w u. { z } ) C ) = ( x e. A |-> ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) ) )
109 nfcv 
 |-  F/_ y ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C )
110 nfcsb1v 
 |-  F/_ x [_ y / x ]_ sum_ m e. w [_ m / k ]_ C
111 nfcv 
 |-  F/_ x +
112 nfcsb1v 
 |-  F/_ x [_ y / x ]_ [_ z / k ]_ C
113 110 111 112 nfov 
 |-  F/_ x ( [_ y / x ]_ sum_ m e. w [_ m / k ]_ C + [_ y / x ]_ [_ z / k ]_ C )
114 csbeq1a 
 |-  ( x = y -> sum_ m e. w [_ m / k ]_ C = [_ y / x ]_ sum_ m e. w [_ m / k ]_ C )
115 csbeq1a 
 |-  ( x = y -> [_ z / k ]_ C = [_ y / x ]_ [_ z / k ]_ C )
116 114 115 oveq12d 
 |-  ( x = y -> ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) = ( [_ y / x ]_ sum_ m e. w [_ m / k ]_ C + [_ y / x ]_ [_ z / k ]_ C ) )
117 109 113 116 cbvmpt 
 |-  ( x e. A |-> ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) ) = ( y e. A |-> ( [_ y / x ]_ sum_ m e. w [_ m / k ]_ C + [_ y / x ]_ [_ z / k ]_ C ) )
118 108 117 eqtrdi 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( x e. A |-> sum_ k e. ( w u. { z } ) C ) = ( y e. A |-> ( [_ y / x ]_ sum_ m e. w [_ m / k ]_ C + [_ y / x ]_ [_ z / k ]_ C ) ) )
119 118 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( x e. A |-> sum_ k e. ( w u. { z } ) C ) = ( y e. A |-> ( [_ y / x ]_ sum_ m e. w [_ m / k ]_ C + [_ y / x ]_ [_ z / k ]_ C ) ) )
120 sumex 
 |-  sum_ m e. w [_ m / k ]_ C e. _V
121 120 csbex 
 |-  [_ y / x ]_ sum_ m e. w [_ m / k ]_ C e. _V
122 121 a1i 
 |-  ( ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) /\ y e. A ) -> [_ y / x ]_ sum_ m e. w [_ m / k ]_ C e. _V )
123 65 66 67 cbvsumi 
 |-  sum_ k e. w C = sum_ m e. w [_ m / k ]_ C
124 123 mpteq2i 
 |-  ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ m e. w [_ m / k ]_ C )
125 nfcv 
 |-  F/_ y sum_ m e. w [_ m / k ]_ C
126 125 110 114 cbvmpt 
 |-  ( x e. A |-> sum_ m e. w [_ m / k ]_ C ) = ( y e. A |-> [_ y / x ]_ sum_ m e. w [_ m / k ]_ C )
127 124 126 eqtri 
 |-  ( x e. A |-> sum_ k e. w C ) = ( y e. A |-> [_ y / x ]_ sum_ m e. w [_ m / k ]_ C )
128 simprl 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( x e. A |-> sum_ k e. w C ) e. L^1 )
129 127 128 eqeltrrid 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( y e. A |-> [_ y / x ]_ sum_ m e. w [_ m / k ]_ C ) e. L^1 )
130 102 elexd 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ x e. A ) -> [_ z / k ]_ C e. _V )
131 130 ralrimiva 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> A. x e. A [_ z / k ]_ C e. _V )
132 131 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> A. x e. A [_ z / k ]_ C e. _V )
133 nfv 
 |-  F/ y [_ z / k ]_ C e. _V
134 112 nfel1 
 |-  F/ x [_ y / x ]_ [_ z / k ]_ C e. _V
135 115 eleq1d 
 |-  ( x = y -> ( [_ z / k ]_ C e. _V <-> [_ y / x ]_ [_ z / k ]_ C e. _V ) )
136 133 134 135 cbvralw 
 |-  ( A. x e. A [_ z / k ]_ C e. _V <-> A. y e. A [_ y / x ]_ [_ z / k ]_ C e. _V )
137 132 136 sylib 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> A. y e. A [_ y / x ]_ [_ z / k ]_ C e. _V )
138 137 r19.21bi 
 |-  ( ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) /\ y e. A ) -> [_ y / x ]_ [_ z / k ]_ C e. _V )
139 nfcv 
 |-  F/_ y [_ z / k ]_ C
140 139 112 115 cbvmpt 
 |-  ( x e. A |-> [_ z / k ]_ C ) = ( y e. A |-> [_ y / x ]_ [_ z / k ]_ C )
141 96 mpteq2dv 
 |-  ( m = z -> ( x e. A |-> [_ m / k ]_ C ) = ( x e. A |-> [_ z / k ]_ C ) )
142 141 eleq1d 
 |-  ( m = z -> ( ( x e. A |-> [_ m / k ]_ C ) e. L^1 <-> ( x e. A |-> [_ z / k ]_ C ) e. L^1 ) )
143 4 ralrimiva 
 |-  ( ph -> A. k e. B ( x e. A |-> C ) e. L^1 )
144 nfv 
 |-  F/ m ( x e. A |-> C ) e. L^1
145 nfcv 
 |-  F/_ k A
146 145 66 nfmpt 
 |-  F/_ k ( x e. A |-> [_ m / k ]_ C )
147 146 nfel1 
 |-  F/ k ( x e. A |-> [_ m / k ]_ C ) e. L^1
148 67 mpteq2dv 
 |-  ( k = m -> ( x e. A |-> C ) = ( x e. A |-> [_ m / k ]_ C ) )
149 148 eleq1d 
 |-  ( k = m -> ( ( x e. A |-> C ) e. L^1 <-> ( x e. A |-> [_ m / k ]_ C ) e. L^1 ) )
150 144 147 149 cbvralw 
 |-  ( A. k e. B ( x e. A |-> C ) e. L^1 <-> A. m e. B ( x e. A |-> [_ m / k ]_ C ) e. L^1 )
151 143 150 sylib 
 |-  ( ph -> A. m e. B ( x e. A |-> [_ m / k ]_ C ) e. L^1 )
152 151 adantr 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> A. m e. B ( x e. A |-> [_ m / k ]_ C ) e. L^1 )
153 142 152 100 rspcdva 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( x e. A |-> [_ z / k ]_ C ) e. L^1 )
154 140 153 eqeltrrid 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( y e. A |-> [_ y / x ]_ [_ z / k ]_ C ) e. L^1 )
155 154 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( y e. A |-> [_ y / x ]_ [_ z / k ]_ C ) e. L^1 )
156 122 129 138 155 ibladd 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( y e. A |-> ( [_ y / x ]_ sum_ m e. w [_ m / k ]_ C + [_ y / x ]_ [_ z / k ]_ C ) ) e. L^1 )
157 119 156 eqeltrd 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 )
158 122 129 138 155 itgadd 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A ( [_ y / x ]_ sum_ m e. w [_ m / k ]_ C + [_ y / x ]_ [_ z / k ]_ C ) _d y = ( S. A [_ y / x ]_ sum_ m e. w [_ m / k ]_ C _d y + S. A [_ y / x ]_ [_ z / k ]_ C _d y ) )
159 116 109 113 cbvitg 
 |-  S. A ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) _d x = S. A ( [_ y / x ]_ sum_ m e. w [_ m / k ]_ C + [_ y / x ]_ [_ z / k ]_ C ) _d y
160 114 125 110 cbvitg 
 |-  S. A sum_ m e. w [_ m / k ]_ C _d x = S. A [_ y / x ]_ sum_ m e. w [_ m / k ]_ C _d y
161 115 139 112 cbvitg 
 |-  S. A [_ z / k ]_ C _d x = S. A [_ y / x ]_ [_ z / k ]_ C _d y
162 160 161 oveq12i 
 |-  ( S. A sum_ m e. w [_ m / k ]_ C _d x + S. A [_ z / k ]_ C _d x ) = ( S. A [_ y / x ]_ sum_ m e. w [_ m / k ]_ C _d y + S. A [_ y / x ]_ [_ z / k ]_ C _d y )
163 158 159 162 3eqtr4g 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) _d x = ( S. A sum_ m e. w [_ m / k ]_ C _d x + S. A [_ z / k ]_ C _d x ) )
164 106 itgeq2dv 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> S. A sum_ m e. ( w u. { z } ) [_ m / k ]_ C _d x = S. A ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) _d x )
165 164 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A sum_ m e. ( w u. { z } ) [_ m / k ]_ C _d x = S. A ( sum_ m e. w [_ m / k ]_ C + [_ z / k ]_ C ) _d x )
166 eqidd 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( w u. { z } ) = ( w u. { z } ) )
167 75 sselda 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ m e. ( w u. { z } ) ) -> m e. B )
168 92 an32s 
 |-  ( ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ m e. B ) /\ x e. A ) -> [_ m / k ]_ C e. CC )
169 152 r19.21bi 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ m e. B ) -> ( x e. A |-> [_ m / k ]_ C ) e. L^1 )
170 168 169 itgcl 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ m e. B ) -> S. A [_ m / k ]_ C _d x e. CC )
171 167 170 syldan 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ m e. ( w u. { z } ) ) -> S. A [_ m / k ]_ C _d x e. CC )
172 71 166 76 171 fsumsplit 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> sum_ m e. ( w u. { z } ) S. A [_ m / k ]_ C _d x = ( sum_ m e. w S. A [_ m / k ]_ C _d x + sum_ m e. { z } S. A [_ m / k ]_ C _d x ) )
173 172 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> sum_ m e. ( w u. { z } ) S. A [_ m / k ]_ C _d x = ( sum_ m e. w S. A [_ m / k ]_ C _d x + sum_ m e. { z } S. A [_ m / k ]_ C _d x ) )
174 simprr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x )
175 itgeq2 
 |-  ( A. x e. A sum_ k e. w C = sum_ m e. w [_ m / k ]_ C -> S. A sum_ k e. w C _d x = S. A sum_ m e. w [_ m / k ]_ C _d x )
176 123 a1i 
 |-  ( x e. A -> sum_ k e. w C = sum_ m e. w [_ m / k ]_ C )
177 175 176 mprg 
 |-  S. A sum_ k e. w C _d x = S. A sum_ m e. w [_ m / k ]_ C _d x
178 nfcv 
 |-  F/_ m S. A C _d x
179 145 66 nfitg 
 |-  F/_ k S. A [_ m / k ]_ C _d x
180 67 adantr 
 |-  ( ( k = m /\ x e. A ) -> C = [_ m / k ]_ C )
181 180 itgeq2dv 
 |-  ( k = m -> S. A C _d x = S. A [_ m / k ]_ C _d x )
182 178 179 181 cbvsumi 
 |-  sum_ k e. w S. A C _d x = sum_ m e. w S. A [_ m / k ]_ C _d x
183 174 177 182 3eqtr3g 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A sum_ m e. w [_ m / k ]_ C _d x = sum_ m e. w S. A [_ m / k ]_ C _d x )
184 102 153 itgcl 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> S. A [_ z / k ]_ C _d x e. CC )
185 184 adantr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A [_ z / k ]_ C _d x e. CC )
186 96 adantr 
 |-  ( ( m = z /\ x e. A ) -> [_ m / k ]_ C = [_ z / k ]_ C )
187 186 itgeq2dv 
 |-  ( m = z -> S. A [_ m / k ]_ C _d x = S. A [_ z / k ]_ C _d x )
188 187 sumsn 
 |-  ( ( z e. _V /\ S. A [_ z / k ]_ C _d x e. CC ) -> sum_ m e. { z } S. A [_ m / k ]_ C _d x = S. A [_ z / k ]_ C _d x )
189 95 185 188 sylancr 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> sum_ m e. { z } S. A [_ m / k ]_ C _d x = S. A [_ z / k ]_ C _d x )
190 189 eqcomd 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A [_ z / k ]_ C _d x = sum_ m e. { z } S. A [_ m / k ]_ C _d x )
191 183 190 oveq12d 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( S. A sum_ m e. w [_ m / k ]_ C _d x + S. A [_ z / k ]_ C _d x ) = ( sum_ m e. w S. A [_ m / k ]_ C _d x + sum_ m e. { z } S. A [_ m / k ]_ C _d x ) )
192 173 191 eqtr4d 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> sum_ m e. ( w u. { z } ) S. A [_ m / k ]_ C _d x = ( S. A sum_ m e. w [_ m / k ]_ C _d x + S. A [_ z / k ]_ C _d x ) )
193 163 165 192 3eqtr4d 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A sum_ m e. ( w u. { z } ) [_ m / k ]_ C _d x = sum_ m e. ( w u. { z } ) S. A [_ m / k ]_ C _d x )
194 itgeq2 
 |-  ( A. x e. A sum_ k e. ( w u. { z } ) C = sum_ m e. ( w u. { z } ) [_ m / k ]_ C -> S. A sum_ k e. ( w u. { z } ) C _d x = S. A sum_ m e. ( w u. { z } ) [_ m / k ]_ C _d x )
195 68 a1i 
 |-  ( x e. A -> sum_ k e. ( w u. { z } ) C = sum_ m e. ( w u. { z } ) [_ m / k ]_ C )
196 194 195 mprg 
 |-  S. A sum_ k e. ( w u. { z } ) C _d x = S. A sum_ m e. ( w u. { z } ) [_ m / k ]_ C _d x
197 178 179 181 cbvsumi 
 |-  sum_ k e. ( w u. { z } ) S. A C _d x = sum_ m e. ( w u. { z } ) S. A [_ m / k ]_ C _d x
198 193 196 197 3eqtr4g 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x )
199 157 198 jca 
 |-  ( ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) /\ ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) )
200 199 ex 
 |-  ( ( ph /\ ( -. z e. w /\ ( w u. { z } ) C_ B ) ) -> ( ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) )
201 200 expr 
 |-  ( ( ph /\ -. z e. w ) -> ( ( w u. { z } ) C_ B -> ( ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) ) )
202 201 a2d 
 |-  ( ( ph /\ -. z e. w ) -> ( ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) ) )
203 64 202 syl5 
 |-  ( ( ph /\ -. z e. w ) -> ( ( w C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) ) )
204 203 expcom 
 |-  ( -. z e. w -> ( ph -> ( ( w C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) ) ) )
205 204 adantl 
 |-  ( ( w e. Fin /\ -. z e. w ) -> ( ph -> ( ( w C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) -> ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) ) ) )
206 205 a2d 
 |-  ( ( w e. Fin /\ -. z e. w ) -> ( ( ph -> ( w C_ B -> ( ( x e. A |-> sum_ k e. w C ) e. L^1 /\ S. A sum_ k e. w C _d x = sum_ k e. w S. A C _d x ) ) ) -> ( ph -> ( ( w u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. ( w u. { z } ) C ) e. L^1 /\ S. A sum_ k e. ( w u. { z } ) C _d x = sum_ k e. ( w u. { z } ) S. A C _d x ) ) ) ) )
207 24 35 46 57 60 206 findcard2s 
 |-  ( B e. Fin -> ( ph -> ( B C_ B -> ( ( x e. A |-> sum_ k e. B C ) e. L^1 /\ S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) ) ) )
208 2 207 mpcom 
 |-  ( ph -> ( B C_ B -> ( ( x e. A |-> sum_ k e. B C ) e. L^1 /\ S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) ) )
209 5 208 mpi 
 |-  ( ph -> ( ( x e. A |-> sum_ k e. B C ) e. L^1 /\ S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) )