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		csbeq1a	\|- ( k = m -> C = [_ m / k ]_ C )
66		nfcv	\|- F/_ m C
67		nfcsb1v	\|- F/_ k [_ m / k ]_ C
68	65 66 67	cbvsum	\|- 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	66	nfel1	\|- F/ m C e. CC
88	67	nfel1	\|- F/ k [_ m / k ]_ C e. CC
89	65	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	cbvsum	\|- 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 67	nfmpt	\|- F/_ k ( x e. A \|-> [_ m / k ]_ C )
147	146	nfel1	\|- F/ k ( x e. A \|-> [_ m / k ]_ C ) e. L^1
148	65	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	65	adantr	\|- ( ( k = m /\ x e. A ) -> C = [_ m / k ]_ C )
179	178	itgeq2dv	\|- ( k = m -> S. A C _d x = S. A [_ m / k ]_ C _d x )
180		nfcv	\|- F/_ m S. A C _d x
181	145 67	nfitg	\|- F/_ k S. A [_ m / k ]_ C _d x
182	179 180 181	cbvsum	\|- 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	179 180 181	cbvsum	\|- 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 ) )

Metamath Proof Explorer

Theorem itgfsum

Proof