Theorem esum2dlem 28964

Description: Lemma for esum2d 28965 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.)

Hypotheses

Ref	Expression
esum2d.0	|- F/_ k F
esum2d.1	|- ( z = <. j , k >. -> F = C )
esum2d.2	|- ( ph -> A e. V )
esum2d.3	|- ( ( ph /\ j e. A ) -> B e. W )
esum2d.4	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
esum2dlem.e	|- ( ph -> A e. Fin )

Assertion

Ref	Expression
esum2dlem	|- ( ph -> Σ* j e. AΣ* k e. B C = Σ* z e. U_ j e. A ( { j } X. B ) F )

Distinct variable groups:   j, k, A, z   z, C   B, k, z   j, F   j, W, k   ph, j, k, z

Allowed substitution hints:   B( j)   C( j, k)   F( z, k)   V( z, j, k)   W( z)

Proof of Theorem esum2dlem

Dummy variables i l t a b are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		esumeq1 28906	. . 3 |- ( a = (/) -> Σ* j e. aΣ* k e. B C = Σ* j e. (/)Σ* k e. B C )
2		nfv 1772	. . . 4 |- F/ z a = (/)
3		iuneq1 4306	. . . 4 |- ( a = (/) -> U_ j e. a ( { j } X. B ) = U_ j e. (/) ( { j } X. B ) )
4	2, 3	esumeq1d 28907	. . 3 |- ( a = (/) -> Σ* z e. U_ j e. a ( { j } X. B ) F = Σ* z e. U_ j e. (/) ( { j } X. B ) F )
5	1, 4	eqeq12d 2477	. 2 |- ( a = (/) -> (Σ* j e. aΣ* k e. B C = Σ* z e. U_ j e. a ( { j } X. B ) F <-> Σ* j e. (/)Σ* k e. B C = Σ* z e. U_ j e. (/) ( { j } X. B ) F ) )
6		esumeq1 28906	. . 3 |- ( a = b -> Σ* j e. aΣ* k e. B C = Σ* j e. bΣ* k e. B C )
7		nfv 1772	. . . 4 |- F/ z a = b
8		iuneq1 4306	. . . 4 |- ( a = b -> U_ j e. a ( { j } X. B ) = U_ j e. b ( { j } X. B ) )
9	7, 8	esumeq1d 28907	. . 3 |- ( a = b -> Σ* z e. U_ j e. a ( { j } X. B ) F = Σ* z e. U_ j e. b ( { j } X. B ) F )
10	6, 9	eqeq12d 2477	. 2 |- ( a = b -> (Σ* j e. aΣ* k e. B C = Σ* z e. U_ j e. a ( { j } X. B ) F <-> Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F ) )
11		esumeq1 28906	. . 3 |- ( a = ( b u. { l } ) -> Σ* j e. aΣ* k e. B C = Σ* j e. ( b u. { l } )Σ* k e. B C )
12		nfv 1772	. . . 4 |- F/ z a = ( b u. { l } )
13		iuneq1 4306	. . . 4 |- ( a = ( b u. { l } ) -> U_ j e. a ( { j } X. B ) = U_ j e. ( b u. { l } ) ( { j } X. B ) )
14	12, 13	esumeq1d 28907	. . 3 |- ( a = ( b u. { l } ) -> Σ* z e. U_ j e. a ( { j } X. B ) F = Σ* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F )
15	11, 14	eqeq12d 2477	. 2 |- ( a = ( b u. { l } ) -> (Σ* j e. aΣ* k e. B C = Σ* z e. U_ j e. a ( { j } X. B ) F <-> Σ* j e. ( b u. { l } )Σ* k e. B C = Σ* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F ) )
16		esumeq1 28906	. . 3 |- ( a = A -> Σ* j e. aΣ* k e. B C = Σ* j e. AΣ* k e. B C )
17		nfv 1772	. . . 4 |- F/ z a = A
18		iuneq1 4306	. . . 4 |- ( a = A -> U_ j e. a ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
19	17, 18	esumeq1d 28907	. . 3 |- ( a = A -> Σ* z e. U_ j e. a ( { j } X. B ) F = Σ* z e. U_ j e. A ( { j } X. B ) F )
20	16, 19	eqeq12d 2477	. 2 |- ( a = A -> (Σ* j e. aΣ* k e. B C = Σ* z e. U_ j e. a ( { j } X. B ) F <-> Σ* j e. AΣ* k e. B C = Σ* z e. U_ j e. A ( { j } X. B ) F ) )
21		esumnul 28920	. . . 4 |- Σ* z e. (/) F = 0
22		0iun 4349	. . . . 5 |- U_ j e. (/) ( { j } X. B ) = (/)
23		esumeq1 28906	. . . . 5 |- ( U_ j e. (/) ( { j } X. B ) = (/) -> Σ* z e. U_ j e. (/) ( { j } X. B ) F = Σ* z e. (/) F )
24	22, 23	ax-mp 5	. . . 4 |- Σ* z e. U_ j e. (/) ( { j } X. B ) F = Σ* z e. (/) F
25		esumnul 28920	. . . 4 |- Σ* j e. (/)Σ* k e. B C = 0
26	21, 24, 25	3eqtr4ri 2495	. . 3 |- Σ* j e. (/)Σ* k e. B C = Σ* z e. U_ j e. (/) ( { j } X. B ) F
27	26	a1i 11	. 2 |- ( ph -> Σ* j e. (/)Σ* k e. B C = Σ* z e. U_ j e. (/) ( { j } X. B ) F )
28		simpr 467	. . . . 5 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F ) -> Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F )
29		nfcsb1v 3391	. . . . . . . . 9 |- F/_ j [_ l / j ]_ B
30		nfcsb1v 3391	. . . . . . . . 9 |- F/_ j [_ l / j ]_ C
31	29, 30	nfesum2 28913	. . . . . . . 8 |- F/_ jΣ* k e. [_ l / j ]_ B [_ l / j ]_ C
32		csbeq1a 3384	. . . . . . . . . 10 |- ( j = l -> B = [_ l / j ]_ B )
33		csbeq1a 3384	. . . . . . . . . 10 |- ( j = l -> C = [_ l / j ]_ C )
34	32, 33	esumeq12d 28905	. . . . . . . . 9 |- ( j = l -> Σ* k e. B C = Σ* k e. [_ l / j ]_ B [_ l / j ]_ C )
35	34	adantl 472	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j = l ) -> Σ* k e. B C = Σ* k e. [_ l / j ]_ B [_ l / j ]_ C )
36		simprr 771	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> l e. ( A \ b ) )
37		difss 3572	. . . . . . . . . . 11 |- ( A \ b ) C_ A
38	37, 36	sseldi 3442	. . . . . . . . . 10 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> l e. A )
39		esum2d.3	. . . . . . . . . . . 12 |- ( ( ph /\ j e. A ) -> B e. W )
40	39	adantlr 726	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. A ) -> B e. W )
41	40	ralrimiva 2814	. . . . . . . . . 10 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. A B e. W )
42		rspcsbela 3807	. . . . . . . . . 10 |- ( ( l e. A /\ A. j e. A B e. W ) -> [_ l / j ]_ B e. W )
43	38, 41, 42	syl2anc 671	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> [_ l / j ]_ B e. W )
44		simpll 765	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> ph )
45	38	adantr 471	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> l e. A )
46		simpr 467	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> k e. [_ l / j ]_ B )
47		esum2d.4	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
48	47	ex 440	. . . . . . . . . . . . . 14 |- ( ph -> ( ( j e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) ) )
49	48	sbcimdv 3341	. . . . . . . . . . . . 13 |- ( ph -> ( [. l / j ]. ( j e. A /\ k e. B ) -> [. l / j ]. C e. ( 0 [,] +oo ) ) )
50		sbcan 3322	. . . . . . . . . . . . . 14 |- ( [. l / j ]. ( j e. A /\ k e. B ) <-> ( [. l / j ]. j e. A /\ [. l / j ]. k e. B ) )
51		sbcel1v 3338	. . . . . . . . . . . . . . 15 |- ( [. l / j ]. j e. A <-> l e. A )
52		sbcel2 3790	. . . . . . . . . . . . . . 15 |- ( [. l / j ]. k e. B <-> k e. [_ l / j ]_ B )
53	51, 52	anbi12i 708	. . . . . . . . . . . . . 14 |- ( ( [. l / j ]. j e. A /\ [. l / j ]. k e. B ) <-> ( l e. A /\ k e. [_ l / j ]_ B ) )
54	50, 53	bitri 257	. . . . . . . . . . . . 13 |- ( [. l / j ]. ( j e. A /\ k e. B ) <-> ( l e. A /\ k e. [_ l / j ]_ B ) )
55		vex 3060	. . . . . . . . . . . . . 14 |- l e. _V
56		sbcel1g 3788	. . . . . . . . . . . . . 14 |- ( l e. _V -> ( [. l / j ]. C e. ( 0 [,] +oo ) <-> [_ l / j ]_ C e. ( 0 [,] +oo ) ) )
57	55, 56	ax-mp 5	. . . . . . . . . . . . 13 |- ( [. l / j ]. C e. ( 0 [,] +oo ) <-> [_ l / j ]_ C e. ( 0 [,] +oo ) )
58	49, 54, 57	3imtr3g 277	. . . . . . . . . . . 12 |- ( ph -> ( ( l e. A /\ k e. [_ l / j ]_ B ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) ) )
59	58	imp 435	. . . . . . . . . . 11 |- ( ( ph /\ ( l e. A /\ k e. [_ l / j ]_ B ) ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) )
60	44, 45, 46, 59	syl12anc 1274	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) )
61	60	ralrimiva 2814	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) )
62		nfcv 2603	. . . . . . . . . 10 |- F/_ k [_ l / j ]_ B
63	62	esumcl 28902	. . . . . . . . 9 |- ( ( [_ l / j ]_ B e. W /\ A. k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) ) -> Σ* k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) )
64	43, 61, 63	syl2anc 671	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Σ* k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) )
65	31, 35, 36, 64	esumsnf 28936	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Σ* j e. { l }Σ* k e. B C = Σ* k e. [_ l / j ]_ B [_ l / j ]_ C )
66		esum2d.0	. . . . . . . . 9 |- F/_ k F
67		nfv 1772	. . . . . . . . 9 |- F/ k ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
68		nfv 1772	. . . . . . . . . . 11 |- F/ j z = <. l , k >.
69	30	nfeq2 2618	. . . . . . . . . . 11 |- F/ j F = [_ l / j ]_ C
70	68, 69	nfim 2014	. . . . . . . . . 10 |- F/ j ( z = <. l , k >. -> F = [_ l / j ]_ C )
71		opeq1 4180	. . . . . . . . . . . 12 |- ( j = l -> <. j , k >. = <. l , k >. )
72	71	eqeq2d 2472	. . . . . . . . . . 11 |- ( j = l -> ( z = <. j , k >. <-> z = <. l , k >. ) )
73	33	eqeq2d 2472	. . . . . . . . . . 11 |- ( j = l -> ( F = C <-> F = [_ l / j ]_ C ) )
74	72, 73	imbi12d 326	. . . . . . . . . 10 |- ( j = l -> ( ( z = <. j , k >. -> F = C ) <-> ( z = <. l , k >. -> F = [_ l / j ]_ C ) ) )
75		esum2d.1	. . . . . . . . . 10 |- ( z = <. j , k >. -> F = C )
76	70, 74, 75	chvar 2117	. . . . . . . . 9 |- ( z = <. l , k >. -> F = [_ l / j ]_ C )
77		ssnid 4009	. . . . . . . . . . . . . . . . . 18 |- j e. { j }
78	77	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> j e. { j } )
79		simpr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> k e. B )
80	78, 79	jca 539	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> ( j e. { j } /\ k e. B ) )
81		opelxp 4886	. . . . . . . . . . . . . . . 16 |- ( <. j , k >. e. ( { j } X. B ) <-> ( j e. { j } /\ k e. B ) )
82	80, 81	sylibr 217	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> <. j , k >. e. ( { j } X. B ) )
83		xp2nd 6856	. . . . . . . . . . . . . . . . 17 |- ( z e. ( { j } X. B ) -> ( 2nd ` z ) e. B )
84	83	adantl 472	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( 2nd ` z ) e. B )
85		eqop 6865	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> ( ( 1st ` z ) = j /\ ( 2nd ` z ) = k ) ) )
86		xp1st 6855	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
87		fvex 5902	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1st ` z ) e. _V
88	87	elsnc 4004	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 1st ` z ) e. { j } <-> ( 1st ` z ) = j )
89	86, 88	sylib 201	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
90	89	biantrurd 515	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( { j } X. B ) -> ( ( 2nd ` z ) = k <-> ( ( 1st ` z ) = j /\ ( 2nd ` z ) = k ) ) )
91	85, 90	bitr4d 264	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> ( 2nd ` z ) = k ) )
92		eqcom 2469	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2nd ` z ) = k <-> k = ( 2nd ` z ) )
93	91, 92	syl6bb 269	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
94	93	ad2antlr 738	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) -> ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
95	94	ralrimiva 2814	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> A. k e. B ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
96		reu6i 3241	. . . . . . . . . . . . . . . 16 |- ( ( ( 2nd ` z ) e. B /\ A. k e. B ( z = <. j , k >. <-> k = ( 2nd ` z ) ) ) -> E! k e. B z = <. j , k >. )
97	84, 95, 96	syl2anc 671	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E! k e. B z = <. j , k >. )
98	82, 97	f1mptrn 28285	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. A ) -> Fun `' ( k e. B |-> <. j , k >. ) )
99	98	ex 440	. . . . . . . . . . . . 13 |- ( ph -> ( j e. A -> Fun `' ( k e. B |-> <. j , k >. ) ) )
100	99	sbcimdv 3341	. . . . . . . . . . . 12 |- ( ph -> ( [. l / j ]. j e. A -> [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) ) )
101		sbcfung 5628	. . . . . . . . . . . . . . 15 |- ( l e. _V -> ( [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) <-> Fun [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) ) )
102		csbcnv 5040	. . . . . . . . . . . . . . . . . 18 |- `' [_ l / j ]_ ( k e. B |-> <. j , k >. ) = [_ l / j ]_ `' ( k e. B |-> <. j , k >. )
103	102	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( l e. _V -> `' [_ l / j ]_ ( k e. B |-> <. j , k >. ) = [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) )
104		csbmpt12 4752	. . . . . . . . . . . . . . . . . . 19 |- ( l e. _V -> [_ l / j ]_ ( k e. B |-> <. j , k >. ) = ( k e. [_ l / j ]_ B |-> [_ l / j ]_ <. j , k >. ) )
105		csbopg 4198	. . . . . . . . . . . . . . . . . . . . 21 |- ( l e. _V -> [_ l / j ]_ <. j , k >. = <. [_ l / j ]_ j , [_ l / j ]_ k >. )
106		csbvarg 3804	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l e. _V -> [_ l / j ]_ j = l )
107		csbconstg 3388	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l e. _V -> [_ l / j ]_ k = k )
108	106, 107	opeq12d 4188	. . . . . . . . . . . . . . . . . . . . 21 |- ( l e. _V -> <. [_ l / j ]_ j , [_ l / j ]_ k >. = <. l , k >. )
109	105, 108	eqtrd 2496	. . . . . . . . . . . . . . . . . . . 20 |- ( l e. _V -> [_ l / j ]_ <. j , k >. = <. l , k >. )
110	109	mpteq2dv 4506	. . . . . . . . . . . . . . . . . . 19 |- ( l e. _V -> ( k e. [_ l / j ]_ B |-> [_ l / j ]_ <. j , k >. ) = ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
111	104, 110	eqtrd 2496	. . . . . . . . . . . . . . . . . 18 |- ( l e. _V -> [_ l / j ]_ ( k e. B |-> <. j , k >. ) = ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
112	111	cnveqd 5032	. . . . . . . . . . . . . . . . 17 |- ( l e. _V -> `' [_ l / j ]_ ( k e. B |-> <. j , k >. ) = `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
113	103, 112	eqtr3d 2498	. . . . . . . . . . . . . . . 16 |- ( l e. _V -> [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) = `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
114	113	funeqd 5626	. . . . . . . . . . . . . . 15 |- ( l e. _V -> ( Fun [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) <-> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
115	101, 114	bitrd 261	. . . . . . . . . . . . . 14 |- ( l e. _V -> ( [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) <-> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
116	55, 115	ax-mp 5	. . . . . . . . . . . . 13 |- ( [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) <-> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
117	51, 116	imbi12i 332	. . . . . . . . . . . 12 |- ( ( [. l / j ]. j e. A -> [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) ) <-> ( l e. A -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
118	100, 117	sylib 201	. . . . . . . . . . 11 |- ( ph -> ( l e. A -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
119	118	imp 435	. . . . . . . . . 10 |- ( ( ph /\ l e. A ) -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
120	38, 119	syldan 477	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
121	55	snid 4008	. . . . . . . . . . . 12 |- l e. { l }
122	121	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> l e. { l } )
123	122, 46	jca 539	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> ( l e. { l } /\ k e. [_ l / j ]_ B ) )
124		opelxp 4886	. . . . . . . . . 10 |- ( <. l , k >. e. ( { l } X. [_ l / j ]_ B ) <-> ( l e. { l } /\ k e. [_ l / j ]_ B ) )
125	123, 124	sylibr 217	. . . . . . . . 9 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> <. l , k >. e. ( { l } X. [_ l / j ]_ B ) )
126	66, 67, 62, 76, 43, 120, 60, 125	esumc 28923	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Σ* k e. [_ l / j ]_ B [_ l / j ]_ C = Σ* z e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } F )
127		nfab1 2605	. . . . . . . . . 10 |- F/_ t { t | E. k e. [_ l / j ]_ B t = <. l , k >. }
128		nfcv 2603	. . . . . . . . . 10 |- F/_ t ( { l } X. [_ l / j ]_ B )
129		opeq1 4180	. . . . . . . . . . . . . 14 |- ( i = l -> <. i , k >. = <. l , k >. )
130	129	eqeq2d 2472	. . . . . . . . . . . . 13 |- ( i = l -> ( t = <. i , k >. <-> t = <. l , k >. ) )
131	130	rexbidv 2913	. . . . . . . . . . . 12 |- ( i = l -> ( E. k e. [_ l / j ]_ B t = <. i , k >. <-> E. k e. [_ l / j ]_ B t = <. l , k >. ) )
132	55, 131	rexsn 4023	. . . . . . . . . . 11 |- ( E. i e. { l } E. k e. [_ l / j ]_ B t = <. i , k >. <-> E. k e. [_ l / j ]_ B t = <. l , k >. )
133		elxp2 4874	. . . . . . . . . . 11 |- ( t e. ( { l } X. [_ l / j ]_ B ) <-> E. i e. { l } E. k e. [_ l / j ]_ B t = <. i , k >. )
134		abid 2450	. . . . . . . . . . 11 |- ( t e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } <-> E. k e. [_ l / j ]_ B t = <. l , k >. )
135	132, 133, 134	3bitr4ri 286	. . . . . . . . . 10 |- ( t e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } <-> t e. ( { l } X. [_ l / j ]_ B ) )
136	127, 128, 135	eqri 28203	. . . . . . . . 9 |- { t | E. k e. [_ l / j ]_ B t = <. l , k >. } = ( { l } X. [_ l / j ]_ B )
137		esumeq1 28906	. . . . . . . . 9 |- ( { t | E. k e. [_ l / j ]_ B t = <. l , k >. } = ( { l } X. [_ l / j ]_ B ) -> Σ* z e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } F = Σ* z e. ( { l } X. [_ l / j ]_ B ) F )
138	136, 137	ax-mp 5	. . . . . . . 8 |- Σ* z e. { t | E. k e. [_ l / j ]_ B t = <. l , k >. } F = Σ* z e. ( { l } X. [_ l / j ]_ B ) F
139	126, 138	syl6eq 2512	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Σ* k e. [_ l / j ]_ B [_ l / j ]_ C = Σ* z e. ( { l } X. [_ l / j ]_ B ) F )
140	65, 139	eqtrd 2496	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Σ* j e. { l }Σ* k e. B C = Σ* z e. ( { l } X. [_ l / j ]_ B ) F )
141	140	adantr 471	. . . . 5 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F ) -> Σ* j e. { l }Σ* k e. B C = Σ* z e. ( { l } X. [_ l / j ]_ B ) F )
142	28, 141	oveq12d 6338	. . . 4 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F ) -> (Σ* j e. bΣ* k e. B C +eΣ* j e. { l }Σ* k e. B C ) = (Σ* z e. U_ j e. b ( { j } X. B ) F +eΣ* z e. ( { l } X. [_ l / j ]_ B ) F ) )
143		nfv 1772	. . . . . 6 |- F/ j ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
144		nfcv 2603	. . . . . 6 |- F/_ j b
145		nfcv 2603	. . . . . 6 |- F/_ j { l }
146		vex 3060	. . . . . . 7 |- b e. _V
147	146	a1i 11	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> b e. _V )
148		snex 4658	. . . . . . 7 |- { l } e. _V
149	148	a1i 11	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> { l } e. _V )
150	36	eldifbd 3429	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> -. l e. b )
151		disjsn 4044	. . . . . . 7 |- ( ( b i^i { l } ) = (/) <-> -. l e. b )
152	150, 151	sylibr 217	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( b i^i { l } ) = (/) )
153		simpll 765	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ph )
154		simprl 769	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> b C_ A )
155	154	sselda 3444	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j e. A )
156	47	anassrs 658	. . . . . . . . 9 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
157	156	ralrimiva 2814	. . . . . . . 8 |- ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) )
158		nfcv 2603	. . . . . . . . 9 |- F/_ k B
159	158	esumcl 28902	. . . . . . . 8 |- ( ( B e. W /\ A. k e. B C e. ( 0 [,] +oo ) ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
160	39, 157, 159	syl2anc 671	. . . . . . 7 |- ( ( ph /\ j e. A ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
161	153, 155, 160	syl2anc 671	. . . . . 6 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
162		simpll 765	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> ph )
163	55	snss 4109	. . . . . . . . 9 |- ( l e. A <-> { l } C_ A )
164	38, 163	sylib 201	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> { l } C_ A )
165	164	sselda 3444	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> j e. A )
166	162, 165, 160	syl2anc 671	. . . . . 6 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
167	143, 144, 145, 147, 149, 152, 161, 166	esumsplit 28925	. . . . 5 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Σ* j e. ( b u. { l } )Σ* k e. B C = (Σ* j e. bΣ* k e. B C +eΣ* j e. { l }Σ* k e. B C ) )
168	167	adantr 471	. . . 4 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F ) -> Σ* j e. ( b u. { l } )Σ* k e. B C = (Σ* j e. bΣ* k e. B C +eΣ* j e. { l }Σ* k e. B C ) )
169		iunxun 4377	. . . . . . . 8 |- U_ j e. ( b u. { l } ) ( { j } X. B ) = ( U_ j e. b ( { j } X. B ) u. U_ j e. { l } ( { j } X. B ) )
170	145, 29	nfxp 4883	. . . . . . . . . . 11 |- F/_ j ( { l } X. [_ l / j ]_ B )
171		sneq 3990	. . . . . . . . . . . 12 |- ( j = l -> { j } = { l } )
172	171, 32	xpeq12d 4881	. . . . . . . . . . 11 |- ( j = l -> ( { j } X. B ) = ( { l } X. [_ l / j ]_ B ) )
173	170, 172	iunxsngf 28227	. . . . . . . . . 10 |- ( l e. _V -> U_ j e. { l } ( { j } X. B ) = ( { l } X. [_ l / j ]_ B ) )
174	55, 173	ax-mp 5	. . . . . . . . 9 |- U_ j e. { l } ( { j } X. B ) = ( { l } X. [_ l / j ]_ B )
175	174	uneq2i 3597	. . . . . . . 8 |- ( U_ j e. b ( { j } X. B ) u. U_ j e. { l } ( { j } X. B ) ) = ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) )
176	169, 175	eqtri 2484	. . . . . . 7 |- U_ j e. ( b u. { l } ) ( { j } X. B ) = ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) )
177		esumeq1 28906	. . . . . . 7 |- ( U_ j e. ( b u. { l } ) ( { j } X. B ) = ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) ) -> Σ* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F = Σ* z e. ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) ) F )
178	176, 177	ax-mp 5	. . . . . 6 |- Σ* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F = Σ* z e. ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) ) F
179		nfv 1772	. . . . . . 7 |- F/ z ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
180		nfcv 2603	. . . . . . 7 |- F/_ z U_ j e. b ( { j } X. B )
181		nfcv 2603	. . . . . . 7 |- F/_ z ( { l } X. [_ l / j ]_ B )
182		snex 4658	. . . . . . . . . 10 |- { j } e. _V
183	155, 40	syldan 477	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> B e. W )
184		xpexg 6625	. . . . . . . . . 10 |- ( ( { j } e. _V /\ B e. W ) -> ( { j } X. B ) e. _V )
185	182, 183, 184	sylancr 674	. . . . . . . . 9 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ( { j } X. B ) e. _V )
186	185	ralrimiva 2814	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. b ( { j } X. B ) e. _V )
187		iunexg 6801	. . . . . . . 8 |- ( ( b e. _V /\ A. j e. b ( { j } X. B ) e. _V ) -> U_ j e. b ( { j } X. B ) e. _V )
188	147, 186, 187	syl2anc 671	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> U_ j e. b ( { j } X. B ) e. _V )
189		xpexg 6625	. . . . . . . 8 |- ( ( { l } e. _V /\ [_ l / j ]_ B e. W ) -> ( { l } X. [_ l / j ]_ B ) e. _V )
190	148, 43, 189	sylancr 674	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( { l } X. [_ l / j ]_ B ) e. _V )
191		simpr 467	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j e. b )
192	150	adantr 471	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> -. l e. b )
193		nelne2 2733	. . . . . . . . . . . 12 |- ( ( j e. b /\ -. l e. b ) -> j =/= l )
194	191, 192, 193	syl2anc 671	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j =/= l )
195		disjsn2 4045	. . . . . . . . . . 11 |- ( j =/= l -> ( { j } i^i { l } ) = (/) )
196		xpdisj1 5280	. . . . . . . . . . 11 |- ( ( { j } i^i { l } ) = (/) -> ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) )
197	194, 195, 196	3syl 18	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) )
198	197	ralrimiva 2814	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. b ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) )
199		iuneq2 4309	. . . . . . . . 9 |- ( A. j e. b ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) -> U_ j e. b ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = U_ j e. b (/) )
200	198, 199	syl 17	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> U_ j e. b ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = U_ j e. b (/) )
201	170	iunin1f 28226	. . . . . . . 8 |- U_ j e. b ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = ( U_ j e. b ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) )
202		iun0 4348	. . . . . . . 8 |- U_ j e. b (/) = (/)
203	200, 201, 202	3eqtr3g 2519	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( U_ j e. b ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) )
204		simpll 765	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> ph )
205		iunss1 4304	. . . . . . . . . 10 |- ( b C_ A -> U_ j e. b ( { j } X. B ) C_ U_ j e. A ( { j } X. B ) )
206	154, 205	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> U_ j e. b ( { j } X. B ) C_ U_ j e. A ( { j } X. B ) )
207	206	sselda 3444	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> z e. U_ j e. A ( { j } X. B ) )
208		nfv 1772	. . . . . . . . . 10 |- F/ j ph
209		nfcv 2603	. . . . . . . . . . 11 |- F/_ j z
210		nfiu1 4322	. . . . . . . . . . 11 |- F/_ j U_ j e. A ( { j } X. B )
211	209, 210	nfel 2615	. . . . . . . . . 10 |- F/ j z e. U_ j e. A ( { j } X. B )
212	208, 211	nfan 2022	. . . . . . . . 9 |- F/ j ( ph /\ z e. U_ j e. A ( { j } X. B ) )
213		nfv 1772	. . . . . . . . . 10 |- F/ k ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) )
214		nfcv 2603	. . . . . . . . . . 11 |- F/_ k ( 0 [,] +oo )
215	66, 214	nfel 2615	. . . . . . . . . 10 |- F/ k F e. ( 0 [,] +oo )
216	75	adantl 472	. . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> F = C )
217		simp-5l 783	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> ph )
218		simp-4r 782	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> j e. A )
219		simplr 767	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> k e. B )
220	217, 218, 219, 47	syl12anc 1274	. . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> C e. ( 0 [,] +oo ) )
221	216, 220	eqeltrd 2540	. . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> F e. ( 0 [,] +oo ) )
222		elsnxp 5401	. . . . . . . . . . . 12 |- ( j e. A -> ( z e. ( { j } X. B ) <-> E. k e. B z = <. j , k >. ) )
223	222	biimpa 491	. . . . . . . . . . 11 |- ( ( j e. A /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. )
224	223	adantll 725	. . . . . . . . . 10 |- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. )
225	213, 215, 221, 224	r19.29af2 2940	. . . . . . . . 9 |- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
226		simpr 467	. . . . . . . . . 10 |- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> z e. U_ j e. A ( { j } X. B ) )
227		eliun 4297	. . . . . . . . . 10 |- ( z e. U_ j e. A ( { j } X. B ) <-> E. j e. A z e. ( { j } X. B ) )
228	226, 227	sylib 201	. . . . . . . . 9 |- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> E. j e. A z e. ( { j } X. B ) )
229	212, 225, 228	r19.29af 2942	. . . . . . . 8 |- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
230	204, 207, 229	syl2anc 671	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
231		simpll 765	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. ( { l } X. [_ l / j ]_ B ) ) -> ph )
232		nfcv 2603	. . . . . . . . . . 11 |- F/_ j A
233		nfcv 2603	. . . . . . . . . . 11 |- F/_ j l
234	232, 233, 170, 172	ssiun2sf 28229	. . . . . . . . . 10 |- ( l e. A -> ( { l } X. [_ l / j ]_ B ) C_ U_ j e. A ( { j } X. B ) )
235	38, 234	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( { l } X. [_ l / j ]_ B ) C_ U_ j e. A ( { j } X. B ) )
236	235	sselda 3444	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. ( { l } X. [_ l / j ]_ B ) ) -> z e. U_ j e. A ( { j } X. B ) )
237	231, 236, 229	syl2anc 671	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. ( { l } X. [_ l / j ]_ B ) ) -> F e. ( 0 [,] +oo ) )
238	179, 180, 181, 188, 190, 203, 230, 237	esumsplit 28925	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Σ* z e. ( U_ j e. b ( { j } X. B ) u. ( { l } X. [_ l / j ]_ B ) ) F = (Σ* z e. U_ j e. b ( { j } X. B ) F +eΣ* z e. ( { l } X. [_ l / j ]_ B ) F ) )
239	178, 238	syl5eq 2508	. . . . 5 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Σ* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F = (Σ* z e. U_ j e. b ( { j } X. B ) F +eΣ* z e. ( { l } X. [_ l / j ]_ B ) F ) )
240	239	adantr 471	. . . 4 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F ) -> Σ* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F = (Σ* z e. U_ j e. b ( { j } X. B ) F +eΣ* z e. ( { l } X. [_ l / j ]_ B ) F ) )
241	142, 168, 240	3eqtr4d 2506	. . 3 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F ) -> Σ* j e. ( b u. { l } )Σ* k e. B C = Σ* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F )
242	241	ex 440	. 2 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> (Σ* j e. bΣ* k e. B C = Σ* z e. U_ j e. b ( { j } X. B ) F -> Σ* j e. ( b u. { l } )Σ* k e. B C = Σ* z e. U_ j e. ( b u. { l } ) ( { j } X. B ) F ) )
243		esum2dlem.e	. 2 |- ( ph -> A e. Fin )
244	5, 10, 15, 20, 27, 242, 243	findcard2d 7844	1 |- ( ph -> Σ* j e. AΣ* k e. B C = Σ* z e. U_ j e. A ( { j } X. B ) F )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   e. wcel 1898   {cab 2448   F/_wnfc 2590   =/= wne 2633   A.wral 2749   E.wrex 2750   E!wreu 2751   _Vcvv 3057   [.wsbc 3279   [_csb 3375   \ cdif 3413   u. cun 3414   i^i cin 3415   C_ wss 3416   (/)c0 3743   {csn 3980   <.cop 3986   U_ciun 4292   |-> cmpt 4477   X. cxp 4854   `'ccnv 4855   Fun wfun 5599   ` cfv 5605  (class class class)co 6320   1stc1st 6823   2ndc2nd 6824   Fincfn 7600   0cc0 9570   +oocpnf 9703   +ecxad 11441   [,]cicc 11672  Σ^*cesum 28899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-pre-sup 9648  ax-addf 9649  ax-mulf 9650

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-of 6563  df-om 6725  df-1st 6825  df-2nd 6826  df-supp 6947  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-2o 7214  df-oadd 7217  df-er 7394  df-map 7505  df-pm 7506  df-ixp 7554  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-fsupp 7915  df-fi 7956  df-sup 7987  df-inf 7988  df-oi 8056  df-card 8404  df-cda 8629  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-7 10706  df-8 10707  df-9 10708  df-10 10709  df-n0 10904  df-z 10972  df-dec 11086  df-uz 11194  df-q 11299  df-rp 11337  df-xneg 11443  df-xadd 11444  df-xmul 11445  df-ioo 11673  df-ioc 11674  df-ico 11675  df-icc 11676  df-fz 11820  df-fzo 11953  df-fl 12066  df-mod 12135  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-shft 13185  df-cj 13217  df-re 13218  df-im 13219  df-sqrt 13353  df-abs 13354  df-limsup 13581  df-clim 13607  df-rlim 13608  df-sum 13808  df-ef 14176  df-sin 14178  df-cos 14179  df-pi 14181  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-ress 15183  df-plusg 15258  df-mulr 15259  df-starv 15260  df-sca 15261  df-vsca 15262  df-ip 15263  df-tset 15264  df-ple 15265  df-ds 15267  df-unif 15268  df-hom 15269  df-cco 15270  df-rest 15376  df-topn 15377  df-0g 15395  df-gsum 15396  df-topgen 15397  df-pt 15398  df-prds 15401  df-ordt 15454  df-xrs 15455  df-qtop 15461  df-imas 15462  df-xps 15465  df-mre 15547  df-mrc 15548  df-acs 15550  df-ps 16501  df-tsr 16502  df-plusf 16542  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-mhm 16637  df-submnd 16638  df-grp 16728  df-minusg 16729  df-sbg 16730  df-mulg 16731  df-subg 16869  df-cntz 17026  df-cmn 17487  df-abl 17488  df-mgp 17779  df-ur 17791  df-ring 17837  df-cring 17838  df-subrg 18061  df-abv 18100  df-lmod 18148  df-scaf 18149  df-sra 18450  df-rgmod 18451  df-psmet 19017  df-xmet 19018  df-met 19019  df-bl 19020  df-mopn 19021  df-fbas 19022  df-fg 19023  df-cnfld 19026  df-top 19976  df-bases 19977  df-topon 19978  df-topsp 19979  df-cld 20089  df-ntr 20090  df-cls 20091  df-nei 20169  df-lp 20207  df-perf 20208  df-cn 20298  df-cnp 20299  df-haus 20386  df-tx 20632  df-hmeo 20825  df-fil 20916  df-fm 21008  df-flim 21009  df-flf 21010  df-tmd 21142  df-tgp 21143  df-tsms 21196  df-trg 21229  df-xms 21390  df-ms 21391  df-tms 21392  df-nm 21652  df-ngp 21653  df-nrg 21655  df-nlm 21656  df-ii 21964  df-cncf 21965  df-limc 22877  df-dv 22878  df-log 23562  df-esum 28900

This theorem is referenced by:  esum2d  28965