Theorem esum2dlem 28921

Description: Lemma for esum2d 28922 (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 28863	. . 3 |- ( a = (/) -> Σ* j e. aΣ* k e. B C = Σ* j e. (/)Σ* k e. B C )
2		nfv 1755	. . . 4 |- F/ z a = (/)
3		iuneq1 4313	. . . 4 |- ( a = (/) -> U_ j e. a ( { j } X. B ) = U_ j e. (/) ( { j } X. B ) )
4	2, 3	esumeq1d 28864	. . 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 2444	. 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 28863	. . 3 |- ( a = b -> Σ* j e. aΣ* k e. B C = Σ* j e. bΣ* k e. B C )
7		nfv 1755	. . . 4 |- F/ z a = b
8		iuneq1 4313	. . . 4 |- ( a = b -> U_ j e. a ( { j } X. B ) = U_ j e. b ( { j } X. B ) )
9	7, 8	esumeq1d 28864	. . 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 2444	. 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 28863	. . 3 |- ( a = ( b u. { l } ) -> Σ* j e. aΣ* k e. B C = Σ* j e. ( b u. { l } )Σ* k e. B C )
12		nfv 1755	. . . 4 |- F/ z a = ( b u. { l } )
13		iuneq1 4313	. . . 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 28864	. . 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 2444	. 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 28863	. . 3 |- ( a = A -> Σ* j e. aΣ* k e. B C = Σ* j e. AΣ* k e. B C )
17		nfv 1755	. . . 4 |- F/ z a = A
18		iuneq1 4313	. . . 4 |- ( a = A -> U_ j e. a ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
19	17, 18	esumeq1d 28864	. . 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 2444	. 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 28877	. . . 4 |- Σ* z e. (/) F = 0
22		0iun 4356	. . . . 5 |- U_ j e. (/) ( { j } X. B ) = (/)
23		esumeq1 28863	. . . . 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 28877	. . . 4 |- Σ* j e. (/)Σ* k e. B C = 0
26	21, 24, 25	3eqtr4ri 2462	. . 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 462	. . . . 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 3411	. . . . . . . . 9 |- F/_ j [_ l / j ]_ B
30		nfcsb1v 3411	. . . . . . . . 9 |- F/_ j [_ l / j ]_ C
31	29, 30	nfesum2 28870	. . . . . . . 8 |- F/_ jΣ* k e. [_ l / j ]_ B [_ l / j ]_ C
32		csbeq1a 3404	. . . . . . . . . 10 |- ( j = l -> B = [_ l / j ]_ B )
33		csbeq1a 3404	. . . . . . . . . 10 |- ( j = l -> C = [_ l / j ]_ C )
34	32, 33	esumeq12d 28862	. . . . . . . . 9 |- ( j = l -> Σ* k e. B C = Σ* k e. [_ l / j ]_ B [_ l / j ]_ C )
35	34	adantl 467	. . . . . . . 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 764	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> l e. ( A \ b ) )
37		difss 3592	. . . . . . . . . . 11 |- ( A \ b ) C_ A
38	37, 36	sseldi 3462	. . . . . . . . . 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 719	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. A ) -> B e. W )
41	40	ralrimiva 2836	. . . . . . . . . 10 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. A B e. W )
42		rspcsbela 3825	. . . . . . . . . 10 |- ( ( l e. A /\ A. j e. A B e. W ) -> [_ l / j ]_ B e. W )
43	38, 41, 42	syl2anc 665	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> [_ l / j ]_ B e. W )
44		simpll 758	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> ph )
45	38	adantr 466	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> l e. A )
46		simpr 462	. . . . . . . . . . 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 435	. . . . . . . . . . . . . 14 |- ( ph -> ( ( j e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) ) )
49	48	sbcimdv 3361	. . . . . . . . . . . . 13 |- ( ph -> ( [. l / j ]. ( j e. A /\ k e. B ) -> [. l / j ]. C e. ( 0 [,] +oo ) ) )
50		sbcan 3342	. . . . . . . . . . . . . 14 |- ( [. l / j ]. ( j e. A /\ k e. B ) <-> ( [. l / j ]. j e. A /\ [. l / j ]. k e. B ) )
51		sbcel1v 3358	. . . . . . . . . . . . . . 15 |- ( [. l / j ]. j e. A <-> l e. A )
52		sbcel2 3808	. . . . . . . . . . . . . . 15 |- ( [. l / j ]. k e. B <-> k e. [_ l / j ]_ B )
53	51, 52	anbi12i 701	. . . . . . . . . . . . . 14 |- ( ( [. l / j ]. j e. A /\ [. l / j ]. k e. B ) <-> ( l e. A /\ k e. [_ l / j ]_ B ) )
54	50, 53	bitri 252	. . . . . . . . . . . . 13 |- ( [. l / j ]. ( j e. A /\ k e. B ) <-> ( l e. A /\ k e. [_ l / j ]_ B ) )
55		vex 3083	. . . . . . . . . . . . . 14 |- l e. _V
56		sbcel1g 3806	. . . . . . . . . . . . . 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 272	. . . . . . . . . . . 12 |- ( ph -> ( ( l e. A /\ k e. [_ l / j ]_ B ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) ) )
59	58	imp 430	. . . . . . . . . . 11 |- ( ( ph /\ ( l e. A /\ k e. [_ l / j ]_ B ) ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) )
60	44, 45, 46, 59	syl12anc 1262	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) )
61	60	ralrimiva 2836	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) )
62		nfcv 2580	. . . . . . . . . 10 |- F/_ k [_ l / j ]_ B
63	62	esumcl 28859	. . . . . . . . 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 665	. . . . . . . 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 28893	. . . . . . 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 1755	. . . . . . . . 9 |- F/ k ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
68		nfv 1755	. . . . . . . . . . 11 |- F/ j z = <. l , k >.
69	30	nfeq2 2597	. . . . . . . . . . 11 |- F/ j F = [_ l / j ]_ C
70	68, 69	nfim 1980	. . . . . . . . . 10 |- F/ j ( z = <. l , k >. -> F = [_ l / j ]_ C )
71		opeq1 4187	. . . . . . . . . . . 12 |- ( j = l -> <. j , k >. = <. l , k >. )
72	71	eqeq2d 2436	. . . . . . . . . . 11 |- ( j = l -> ( z = <. j , k >. <-> z = <. l , k >. ) )
73	33	eqeq2d 2436	. . . . . . . . . . 11 |- ( j = l -> ( F = C <-> F = [_ l / j ]_ C ) )
74	72, 73	imbi12d 321	. . . . . . . . . 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 2071	. . . . . . . . 9 |- ( z = <. l , k >. -> F = [_ l / j ]_ C )
77		ssnid 4027	. . . . . . . . . . . . . . . . . 18 |- j e. { j }
78	77	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> j e. { j } )
79		simpr 462	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> k e. B )
80	78, 79	jca 534	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> ( j e. { j } /\ k e. B ) )
81		opelxp 4883	. . . . . . . . . . . . . . . 16 |- ( <. j , k >. e. ( { j } X. B ) <-> ( j e. { j } /\ k e. B ) )
82	80, 81	sylibr 215	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> <. j , k >. e. ( { j } X. B ) )
83		xp2nd 6838	. . . . . . . . . . . . . . . . 17 |- ( z e. ( { j } X. B ) -> ( 2nd ` z ) e. B )
84	83	adantl 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( 2nd ` z ) e. B )
85		eqop 6847	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> ( ( 1st ` z ) = j /\ ( 2nd ` z ) = k ) ) )
86		xp1st 6837	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
87		fvex 5891	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1st ` z ) e. _V
88	87	elsnc 4022	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 1st ` z ) e. { j } <-> ( 1st ` z ) = j )
89	86, 88	sylib 199	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
90	89	biantrurd 510	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( { j } X. B ) -> ( ( 2nd ` z ) = k <-> ( ( 1st ` z ) = j /\ ( 2nd ` z ) = k ) ) )
91	85, 90	bitr4d 259	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> ( 2nd ` z ) = k ) )
92		eqcom 2431	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2nd ` z ) = k <-> k = ( 2nd ` z ) )
93	91, 92	syl6bb 264	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
94	93	ad2antlr 731	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) -> ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
95	94	ralrimiva 2836	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> A. k e. B ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
96		reu6i 3261	. . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E! k e. B z = <. j , k >. )
98	82, 97	f1mptrn 28234	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. A ) -> Fun `' ( k e. B |-> <. j , k >. ) )
99	98	ex 435	. . . . . . . . . . . . 13 |- ( ph -> ( j e. A -> Fun `' ( k e. B |-> <. j , k >. ) ) )
100	99	sbcimdv 3361	. . . . . . . . . . . 12 |- ( ph -> ( [. l / j ]. j e. A -> [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) ) )
101		sbcfung 5624	. . . . . . . . . . . . . . 15 |- ( l e. _V -> ( [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) <-> Fun [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) ) )
102		csbcnv 5037	. . . . . . . . . . . . . . . . . 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 4754	. . . . . . . . . . . . . . . . . . 19 |- ( l e. _V -> [_ l / j ]_ ( k e. B |-> <. j , k >. ) = ( k e. [_ l / j ]_ B |-> [_ l / j ]_ <. j , k >. ) )
105		csbopg 4205	. . . . . . . . . . . . . . . . . . . . 21 |- ( l e. _V -> [_ l / j ]_ <. j , k >. = <. [_ l / j ]_ j , [_ l / j ]_ k >. )
106		csbvarg 3822	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l e. _V -> [_ l / j ]_ j = l )
107		csbconstg 3408	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l e. _V -> [_ l / j ]_ k = k )
108	106, 107	opeq12d 4195	. . . . . . . . . . . . . . . . . . . . 21 |- ( l e. _V -> <. [_ l / j ]_ j , [_ l / j ]_ k >. = <. l , k >. )
109	105, 108	eqtrd 2463	. . . . . . . . . . . . . . . . . . . 20 |- ( l e. _V -> [_ l / j ]_ <. j , k >. = <. l , k >. )
110	109	mpteq2dv 4511	. . . . . . . . . . . . . . . . . . 19 |- ( l e. _V -> ( k e. [_ l / j ]_ B |-> [_ l / j ]_ <. j , k >. ) = ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
111	104, 110	eqtrd 2463	. . . . . . . . . . . . . . . . . 18 |- ( l e. _V -> [_ l / j ]_ ( k e. B |-> <. j , k >. ) = ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
112	111	cnveqd 5029	. . . . . . . . . . . . . . . . 17 |- ( l e. _V -> `' [_ l / j ]_ ( k e. B |-> <. j , k >. ) = `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
113	103, 112	eqtr3d 2465	. . . . . . . . . . . . . . . 16 |- ( l e. _V -> [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) = `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
114	113	funeqd 5622	. . . . . . . . . . . . . . 15 |- ( l e. _V -> ( Fun [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) <-> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
115	101, 114	bitrd 256	. . . . . . . . . . . . . 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 327	. . . . . . . . . . . 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 199	. . . . . . . . . . 11 |- ( ph -> ( l e. A -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
119	118	imp 430	. . . . . . . . . 10 |- ( ( ph /\ l e. A ) -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
120	38, 119	syldan 472	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
121	55	snid 4026	. . . . . . . . . . . 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 534	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> ( l e. { l } /\ k e. [_ l / j ]_ B ) )
124		opelxp 4883	. . . . . . . . . 10 |- ( <. l , k >. e. ( { l } X. [_ l / j ]_ B ) <-> ( l e. { l } /\ k e. [_ l / j ]_ B ) )
125	123, 124	sylibr 215	. . . . . . . . 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 28880	. . . . . . . 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 2582	. . . . . . . . . 10 |- F/_ t { t | E. k e. [_ l / j ]_ B t = <. l , k >. }
128		nfcv 2580	. . . . . . . . . 10 |- F/_ t ( { l } X. [_ l / j ]_ B )
129		opeq1 4187	. . . . . . . . . . . . . 14 |- ( i = l -> <. i , k >. = <. l , k >. )
130	129	eqeq2d 2436	. . . . . . . . . . . . 13 |- ( i = l -> ( t = <. i , k >. <-> t = <. l , k >. ) )
131	130	rexbidv 2936	. . . . . . . . . . . 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 4039	. . . . . . . . . . 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 4871	. . . . . . . . . . 11 |- ( t e. ( { l } X. [_ l / j ]_ B ) <-> E. i e. { l } E. k e. [_ l / j ]_ B t = <. i , k >. )
134		abid 2409	. . . . . . . . . . 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 281	. . . . . . . . . 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 28146	. . . . . . . . 9 |- { t | E. k e. [_ l / j ]_ B t = <. l , k >. } = ( { l } X. [_ l / j ]_ B )
137		esumeq1 28863	. . . . . . . . 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 2479	. . . . . . 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 2463	. . . . . 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 466	. . . . 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 6323	. . . 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 1755	. . . . . 6 |- F/ j ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
144		nfcv 2580	. . . . . 6 |- F/_ j b
145		nfcv 2580	. . . . . 6 |- F/_ j { l }
146		vex 3083	. . . . . . 7 |- b e. _V
147	146	a1i 11	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> b e. _V )
148		snex 4662	. . . . . . 7 |- { l } e. _V
149	148	a1i 11	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> { l } e. _V )
150	36	eldifbd 3449	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> -. l e. b )
151		disjsn 4060	. . . . . . 7 |- ( ( b i^i { l } ) = (/) <-> -. l e. b )
152	150, 151	sylibr 215	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( b i^i { l } ) = (/) )
153		simpll 758	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ph )
154		simprl 762	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> b C_ A )
155	154	sselda 3464	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j e. A )
156	47	anassrs 652	. . . . . . . . 9 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
157	156	ralrimiva 2836	. . . . . . . 8 |- ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) )
158		nfcv 2580	. . . . . . . . 9 |- F/_ k B
159	158	esumcl 28859	. . . . . . . 8 |- ( ( B e. W /\ A. k e. B C e. ( 0 [,] +oo ) ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
160	39, 157, 159	syl2anc 665	. . . . . . 7 |- ( ( ph /\ j e. A ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
161	153, 155, 160	syl2anc 665	. . . . . 6 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
162		simpll 758	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> ph )
163	55	snss 4124	. . . . . . . . 9 |- ( l e. A <-> { l } C_ A )
164	38, 163	sylib 199	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> { l } C_ A )
165	164	sselda 3464	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> j e. A )
166	162, 165, 160	syl2anc 665	. . . . . 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 28882	. . . . 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 466	. . . 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 4384	. . . . . . . 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 4880	. . . . . . . . . . 11 |- F/_ j ( { l } X. [_ l / j ]_ B )
171		sneq 4008	. . . . . . . . . . . 12 |- ( j = l -> { j } = { l } )
172	171, 32	xpeq12d 4878	. . . . . . . . . . 11 |- ( j = l -> ( { j } X. B ) = ( { l } X. [_ l / j ]_ B ) )
173	170, 172	iunxsngf 28174	. . . . . . . . . 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 3617	. . . . . . . 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 2451	. . . . . . 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 28863	. . . . . . 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 1755	. . . . . . 7 |- F/ z ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
180		nfcv 2580	. . . . . . 7 |- F/_ z U_ j e. b ( { j } X. B )
181		nfcv 2580	. . . . . . 7 |- F/_ z ( { l } X. [_ l / j ]_ B )
182		snex 4662	. . . . . . . . . 10 |- { j } e. _V
183	155, 40	syldan 472	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> B e. W )
184		xpexg 6607	. . . . . . . . . 10 |- ( ( { j } e. _V /\ B e. W ) -> ( { j } X. B ) e. _V )
185	182, 183, 184	sylancr 667	. . . . . . . . 9 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ( { j } X. B ) e. _V )
186	185	ralrimiva 2836	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. b ( { j } X. B ) e. _V )
187		iunexg 6783	. . . . . . . 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 665	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> U_ j e. b ( { j } X. B ) e. _V )
189		xpexg 6607	. . . . . . . 8 |- ( ( { l } e. _V /\ [_ l / j ]_ B e. W ) -> ( { l } X. [_ l / j ]_ B ) e. _V )
190	148, 43, 189	sylancr 667	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( { l } X. [_ l / j ]_ B ) e. _V )
191		simpr 462	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j e. b )
192	150	adantr 466	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> -. l e. b )
193		nelne2 2750	. . . . . . . . . . . 12 |- ( ( j e. b /\ -. l e. b ) -> j =/= l )
194	191, 192, 193	syl2anc 665	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j =/= l )
195		disjsn2 4061	. . . . . . . . . . 11 |- ( j =/= l -> ( { j } i^i { l } ) = (/) )
196		xpdisj1 5277	. . . . . . . . . . 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 2836	. . . . . . . . 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 4316	. . . . . . . . 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 28173	. . . . . . . 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 4355	. . . . . . . 8 |- U_ j e. b (/) = (/)
203	200, 201, 202	3eqtr3g 2486	. . . . . . 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 758	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> ph )
205		iunss1 4311	. . . . . . . . . 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 3464	. . . . . . . 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 1755	. . . . . . . . . 10 |- F/ j ph
209		nfcv 2580	. . . . . . . . . . 11 |- F/_ j z
210		nfiu1 4329	. . . . . . . . . . 11 |- F/_ j U_ j e. A ( { j } X. B )
211	209, 210	nfel 2593	. . . . . . . . . 10 |- F/ j z e. U_ j e. A ( { j } X. B )
212	208, 211	nfan 1988	. . . . . . . . 9 |- F/ j ( ph /\ z e. U_ j e. A ( { j } X. B ) )
213		nfv 1755	. . . . . . . . . 10 |- F/ k ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) )
214		nfcv 2580	. . . . . . . . . . 11 |- F/_ k ( 0 [,] +oo )
215	66, 214	nfel 2593	. . . . . . . . . 10 |- F/ k F e. ( 0 [,] +oo )
216	75	adantl 467	. . . . . . . . . . 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 776	. . . . . . . . . . . 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 775	. . . . . . . . . . . 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 760	. . . . . . . . . . . 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 1262	. . . . . . . . . . 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 2507	. . . . . . . . . 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 5397	. . . . . . . . . . . 12 |- ( j e. A -> ( z e. ( { j } X. B ) <-> E. k e. B z = <. j , k >. ) )
223	222	biimpa 486	. . . . . . . . . . 11 |- ( ( j e. A /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. )
224	223	adantll 718	. . . . . . . . . 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 2963	. . . . . . . . 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 462	. . . . . . . . . 10 |- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> z e. U_ j e. A ( { j } X. B ) )
227		eliun 4304	. . . . . . . . . 10 |- ( z e. U_ j e. A ( { j } X. B ) <-> E. j e. A z e. ( { j } X. B ) )
228	226, 227	sylib 199	. . . . . . . . 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 2965	. . . . . . . 8 |- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
230	204, 207, 229	syl2anc 665	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
231		simpll 758	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. ( { l } X. [_ l / j ]_ B ) ) -> ph )
232		nfcv 2580	. . . . . . . . . . 11 |- F/_ j A
233		nfcv 2580	. . . . . . . . . . 11 |- F/_ j l
234	232, 233, 170, 172	ssiun2sf 28176	. . . . . . . . . 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 3464	. . . . . . . 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 665	. . . . . . 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 28882	. . . . . 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 2475	. . . . 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 466	. . . 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 2473	. . 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 435	. 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 7822	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 187   /\ wa 370   = wceq 1437   e. wcel 1872   {cab 2407   F/_wnfc 2566   =/= wne 2614   A.wral 2771   E.wrex 2772   E!wreu 2773   _Vcvv 3080   [.wsbc 3299   [_csb 3395   \ cdif 3433   u. cun 3434   i^i cin 3435   C_ wss 3436   (/)c0 3761   {csn 3998   <.cop 4004   U_ciun 4299   |-> cmpt 4482   X. cxp 4851   `'ccnv 4852   Fun wfun 5595   ` cfv 5601  (class class class)co 6305   1stc1st 6805   2ndc2nd 6806   Fincfn 7580   0cc0 9546   +oocpnf 9679   +ecxad 11414   [,]cicc 11645  Σ^*cesum 28856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-inf2 8155  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623  ax-pre-sup 9624  ax-addf 9625  ax-mulf 9626

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-iin 4302  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-of 6545  df-om 6707  df-1st 6807  df-2nd 6808  df-supp 6926  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-2o 7194  df-oadd 7197  df-er 7374  df-map 7485  df-pm 7486  df-ixp 7534  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584  df-fsupp 7893  df-fi 7934  df-sup 7965  df-inf 7966  df-oi 8034  df-card 8381  df-cda 8605  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-4 10677  df-5 10678  df-6 10679  df-7 10680  df-8 10681  df-9 10682  df-10 10683  df-n0 10877  df-z 10945  df-dec 11059  df-uz 11167  df-q 11272  df-rp 11310  df-xneg 11416  df-xadd 11417  df-xmul 11418  df-ioo 11646  df-ioc 11647  df-ico 11648  df-icc 11649  df-fz 11792  df-fzo 11923  df-fl 12034  df-mod 12103  df-seq 12220  df-exp 12279  df-fac 12466  df-bc 12494  df-hash 12522  df-shft 13130  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-limsup 13525  df-clim 13551  df-rlim 13552  df-sum 13752  df-ef 14120  df-sin 14122  df-cos 14123  df-pi 14125  df-struct 15122  df-ndx 15123  df-slot 15124  df-base 15125  df-sets 15126  df-ress 15127  df-plusg 15202  df-mulr 15203  df-starv 15204  df-sca 15205  df-vsca 15206  df-ip 15207  df-tset 15208  df-ple 15209  df-ds 15211  df-unif 15212  df-hom 15213  df-cco 15214  df-rest 15320  df-topn 15321  df-0g 15339  df-gsum 15340  df-topgen 15341  df-pt 15342  df-prds 15345  df-ordt 15398  df-xrs 15399  df-qtop 15405  df-imas 15406  df-xps 15409  df-mre 15491  df-mrc 15492  df-acs 15494  df-ps 16445  df-tsr 16446  df-plusf 16486  df-mgm 16487  df-sgrp 16526  df-mnd 16536  df-mhm 16581  df-submnd 16582  df-grp 16672  df-minusg 16673  df-sbg 16674  df-mulg 16675  df-subg 16813  df-cntz 16970  df-cmn 17431  df-abl 17432  df-mgp 17723  df-ur 17735  df-ring 17781  df-cring 17782  df-subrg 18005  df-abv 18044  df-lmod 18092  df-scaf 18093  df-sra 18394  df-rgmod 18395  df-psmet 18961  df-xmet 18962  df-met 18963  df-bl 18964  df-mopn 18965  df-fbas 18966  df-fg 18967  df-cnfld 18970  df-top 19919  df-bases 19920  df-topon 19921  df-topsp 19922  df-cld 20032  df-ntr 20033  df-cls 20034  df-nei 20112  df-lp 20150  df-perf 20151  df-cn 20241  df-cnp 20242  df-haus 20329  df-tx 20575  df-hmeo 20768  df-fil 20859  df-fm 20951  df-flim 20952  df-flf 20953  df-tmd 21085  df-tgp 21086  df-tsms 21139  df-trg 21172  df-xms 21333  df-ms 21334  df-tms 21335  df-nm 21595  df-ngp 21596  df-nrg 21598  df-nlm 21599  df-ii 21907  df-cncf 21908  df-limc 22819  df-dv 22820  df-log 23504  df-esum 28857

This theorem is referenced by:  esum2d  28922