Theorem esum2dlem 28525

Description: Lemma for esum2d 28526 (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 28467	. . 3 |- ( a = (/) -> Σ* j e. aΣ* k e. B C = Σ* j e. (/)Σ* k e. B C )
2		nfv 1728	. . . 4 |- F/ z a = (/)
3		iuneq1 4284	. . . 4 |- ( a = (/) -> U_ j e. a ( { j } X. B ) = U_ j e. (/) ( { j } X. B ) )
4	2, 3	esumeq1d 28468	. . 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 2424	. 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 28467	. . 3 |- ( a = b -> Σ* j e. aΣ* k e. B C = Σ* j e. bΣ* k e. B C )
7		nfv 1728	. . . 4 |- F/ z a = b
8		iuneq1 4284	. . . 4 |- ( a = b -> U_ j e. a ( { j } X. B ) = U_ j e. b ( { j } X. B ) )
9	7, 8	esumeq1d 28468	. . 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 2424	. 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 28467	. . 3 |- ( a = ( b u. { l } ) -> Σ* j e. aΣ* k e. B C = Σ* j e. ( b u. { l } )Σ* k e. B C )
12		nfv 1728	. . . 4 |- F/ z a = ( b u. { l } )
13		iuneq1 4284	. . . 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 28468	. . 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 2424	. 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 28467	. . 3 |- ( a = A -> Σ* j e. aΣ* k e. B C = Σ* j e. AΣ* k e. B C )
17		nfv 1728	. . . 4 |- F/ z a = A
18		iuneq1 4284	. . . 4 |- ( a = A -> U_ j e. a ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
19	17, 18	esumeq1d 28468	. . 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 2424	. 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 28481	. . . 4 |- Σ* z e. (/) F = 0
22		0iun 4327	. . . . 5 |- U_ j e. (/) ( { j } X. B ) = (/)
23		esumeq1 28467	. . . . 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 28481	. . . 4 |- Σ* j e. (/)Σ* k e. B C = 0
26	21, 24, 25	3eqtr4ri 2442	. . 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 459	. . . . 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 3388	. . . . . . . . 9 |- F/_ j [_ l / j ]_ B
30		nfcsb1v 3388	. . . . . . . . 9 |- F/_ j [_ l / j ]_ C
31	29, 30	nfesum2 28474	. . . . . . . 8 |- F/_ jΣ* k e. [_ l / j ]_ B [_ l / j ]_ C
32		csbeq1a 3381	. . . . . . . . . 10 |- ( j = l -> B = [_ l / j ]_ B )
33		csbeq1a 3381	. . . . . . . . . 10 |- ( j = l -> C = [_ l / j ]_ C )
34	32, 33	esumeq12d 28466	. . . . . . . . 9 |- ( j = l -> Σ* k e. B C = Σ* k e. [_ l / j ]_ B [_ l / j ]_ C )
35	34	adantl 464	. . . . . . . 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 758	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> l e. ( A \ b ) )
37		difss 3569	. . . . . . . . . . 11 |- ( A \ b ) C_ A
38	37, 36	sseldi 3439	. . . . . . . . . 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 713	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. A ) -> B e. W )
41	40	ralrimiva 2817	. . . . . . . . . 10 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. A B e. W )
42		rspcsbela 3799	. . . . . . . . . 10 |- ( ( l e. A /\ A. j e. A B e. W ) -> [_ l / j ]_ B e. W )
43	38, 41, 42	syl2anc 659	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> [_ l / j ]_ B e. W )
44		simpll 752	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> ph )
45	38	adantr 463	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> l e. A )
46		simpr 459	. . . . . . . . . . 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 432	. . . . . . . . . . . . . 14 |- ( ph -> ( ( j e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) ) )
49	48	sbcimdv 3338	. . . . . . . . . . . . 13 |- ( ph -> ( [. l / j ]. ( j e. A /\ k e. B ) -> [. l / j ]. C e. ( 0 [,] +oo ) ) )
50		sbcan 3319	. . . . . . . . . . . . . 14 |- ( [. l / j ]. ( j e. A /\ k e. B ) <-> ( [. l / j ]. j e. A /\ [. l / j ]. k e. B ) )
51		sbcel1v 3335	. . . . . . . . . . . . . . 15 |- ( [. l / j ]. j e. A <-> l e. A )
52		sbcel2 3782	. . . . . . . . . . . . . . 15 |- ( [. l / j ]. k e. B <-> k e. [_ l / j ]_ B )
53	51, 52	anbi12i 695	. . . . . . . . . . . . . 14 |- ( ( [. l / j ]. j e. A /\ [. l / j ]. k e. B ) <-> ( l e. A /\ k e. [_ l / j ]_ B ) )
54	50, 53	bitri 249	. . . . . . . . . . . . 13 |- ( [. l / j ]. ( j e. A /\ k e. B ) <-> ( l e. A /\ k e. [_ l / j ]_ B ) )
55		vex 3061	. . . . . . . . . . . . . 14 |- l e. _V
56		sbcel1g 3780	. . . . . . . . . . . . . 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 269	. . . . . . . . . . . 12 |- ( ph -> ( ( l e. A /\ k e. [_ l / j ]_ B ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) ) )
59	58	imp 427	. . . . . . . . . . 11 |- ( ( ph /\ ( l e. A /\ k e. [_ l / j ]_ B ) ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) )
60	44, 45, 46, 59	syl12anc 1228	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> [_ l / j ]_ C e. ( 0 [,] +oo ) )
61	60	ralrimiva 2817	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. k e. [_ l / j ]_ B [_ l / j ]_ C e. ( 0 [,] +oo ) )
62		nfcv 2564	. . . . . . . . . 10 |- F/_ k [_ l / j ]_ B
63	62	esumcl 28463	. . . . . . . . 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 659	. . . . . . . 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 28497	. . . . . . 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 1728	. . . . . . . . 9 |- F/ k ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
68		nfv 1728	. . . . . . . . . . 11 |- F/ j z = <. l , k >.
69	30	nfeq2 2581	. . . . . . . . . . 11 |- F/ j F = [_ l / j ]_ C
70	68, 69	nfim 1948	. . . . . . . . . 10 |- F/ j ( z = <. l , k >. -> F = [_ l / j ]_ C )
71		opeq1 4158	. . . . . . . . . . . 12 |- ( j = l -> <. j , k >. = <. l , k >. )
72	71	eqeq2d 2416	. . . . . . . . . . 11 |- ( j = l -> ( z = <. j , k >. <-> z = <. l , k >. ) )
73	33	eqeq2d 2416	. . . . . . . . . . 11 |- ( j = l -> ( F = C <-> F = [_ l / j ]_ C ) )
74	72, 73	imbi12d 318	. . . . . . . . . 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 2040	. . . . . . . . 9 |- ( z = <. l , k >. -> F = [_ l / j ]_ C )
77		ssnid 4000	. . . . . . . . . . . . . . . . . 18 |- j e. { j }
78	77	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> j e. { j } )
79		simpr 459	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> k e. B )
80	78, 79	jca 530	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> ( j e. { j } /\ k e. B ) )
81		opelxp 4852	. . . . . . . . . . . . . . . 16 |- ( <. j , k >. e. ( { j } X. B ) <-> ( j e. { j } /\ k e. B ) )
82	80, 81	sylibr 212	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> <. j , k >. e. ( { j } X. B ) )
83		xp2nd 6814	. . . . . . . . . . . . . . . . 17 |- ( z e. ( { j } X. B ) -> ( 2nd ` z ) e. B )
84	83	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( 2nd ` z ) e. B )
85		eqop 6823	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> ( ( 1st ` z ) = j /\ ( 2nd ` z ) = k ) ) )
86		xp1st 6813	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
87		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1st ` z ) e. _V
88	87	elsnc 3995	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 1st ` z ) e. { j } <-> ( 1st ` z ) = j )
89	86, 88	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
90	89	biantrurd 506	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( { j } X. B ) -> ( ( 2nd ` z ) = k <-> ( ( 1st ` z ) = j /\ ( 2nd ` z ) = k ) ) )
91	85, 90	bitr4d 256	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> ( 2nd ` z ) = k ) )
92		eqcom 2411	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2nd ` z ) = k <-> k = ( 2nd ` z ) )
93	91, 92	syl6bb 261	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( { j } X. B ) -> ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
94	93	ad2antlr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) -> ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
95	94	ralrimiva 2817	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> A. k e. B ( z = <. j , k >. <-> k = ( 2nd ` z ) ) )
96		reu6i 3239	. . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E! k e. B z = <. j , k >. )
98	82, 97	f1mptrn 27901	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. A ) -> Fun `' ( k e. B |-> <. j , k >. ) )
99	98	ex 432	. . . . . . . . . . . . 13 |- ( ph -> ( j e. A -> Fun `' ( k e. B |-> <. j , k >. ) ) )
100	99	sbcimdv 3338	. . . . . . . . . . . 12 |- ( ph -> ( [. l / j ]. j e. A -> [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) ) )
101		sbcfung 5591	. . . . . . . . . . . . . . 15 |- ( l e. _V -> ( [. l / j ]. Fun `' ( k e. B |-> <. j , k >. ) <-> Fun [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) ) )
102		csbcnv 5006	. . . . . . . . . . . . . . . . . 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 4723	. . . . . . . . . . . . . . . . . . 19 |- ( l e. _V -> [_ l / j ]_ ( k e. B |-> <. j , k >. ) = ( k e. [_ l / j ]_ B |-> [_ l / j ]_ <. j , k >. ) )
105		csbopg 4176	. . . . . . . . . . . . . . . . . . . . 21 |- ( l e. _V -> [_ l / j ]_ <. j , k >. = <. [_ l / j ]_ j , [_ l / j ]_ k >. )
106		csbvarg 3796	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l e. _V -> [_ l / j ]_ j = l )
107		csbconstg 3385	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l e. _V -> [_ l / j ]_ k = k )
108	106, 107	opeq12d 4166	. . . . . . . . . . . . . . . . . . . . 21 |- ( l e. _V -> <. [_ l / j ]_ j , [_ l / j ]_ k >. = <. l , k >. )
109	105, 108	eqtrd 2443	. . . . . . . . . . . . . . . . . . . 20 |- ( l e. _V -> [_ l / j ]_ <. j , k >. = <. l , k >. )
110	109	mpteq2dv 4481	. . . . . . . . . . . . . . . . . . 19 |- ( l e. _V -> ( k e. [_ l / j ]_ B |-> [_ l / j ]_ <. j , k >. ) = ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
111	104, 110	eqtrd 2443	. . . . . . . . . . . . . . . . . 18 |- ( l e. _V -> [_ l / j ]_ ( k e. B |-> <. j , k >. ) = ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
112	111	cnveqd 4998	. . . . . . . . . . . . . . . . 17 |- ( l e. _V -> `' [_ l / j ]_ ( k e. B |-> <. j , k >. ) = `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
113	103, 112	eqtr3d 2445	. . . . . . . . . . . . . . . 16 |- ( l e. _V -> [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) = `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
114	113	funeqd 5589	. . . . . . . . . . . . . . 15 |- ( l e. _V -> ( Fun [_ l / j ]_ `' ( k e. B |-> <. j , k >. ) <-> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
115	101, 114	bitrd 253	. . . . . . . . . . . . . 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 324	. . . . . . . . . . . 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 196	. . . . . . . . . . 11 |- ( ph -> ( l e. A -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) ) )
119	118	imp 427	. . . . . . . . . 10 |- ( ( ph /\ l e. A ) -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
120	38, 119	syldan 468	. . . . . . . . 9 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> Fun `' ( k e. [_ l / j ]_ B |-> <. l , k >. ) )
121	55	snid 3999	. . . . . . . . . . . 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 530	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ k e. [_ l / j ]_ B ) -> ( l e. { l } /\ k e. [_ l / j ]_ B ) )
124		opelxp 4852	. . . . . . . . . 10 |- ( <. l , k >. e. ( { l } X. [_ l / j ]_ B ) <-> ( l e. { l } /\ k e. [_ l / j ]_ B ) )
125	123, 124	sylibr 212	. . . . . . . . 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 28484	. . . . . . . 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 2566	. . . . . . . . . 10 |- F/_ t { t | E. k e. [_ l / j ]_ B t = <. l , k >. }
128		nfcv 2564	. . . . . . . . . 10 |- F/_ t ( { l } X. [_ l / j ]_ B )
129		opeq1 4158	. . . . . . . . . . . . . 14 |- ( i = l -> <. i , k >. = <. l , k >. )
130	129	eqeq2d 2416	. . . . . . . . . . . . 13 |- ( i = l -> ( t = <. i , k >. <-> t = <. l , k >. ) )
131	130	rexbidv 2917	. . . . . . . . . . . 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 4011	. . . . . . . . . . 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 4840	. . . . . . . . . . 11 |- ( t e. ( { l } X. [_ l / j ]_ B ) <-> E. i e. { l } E. k e. [_ l / j ]_ B t = <. i , k >. )
134		abid 2389	. . . . . . . . . . 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 278	. . . . . . . . . 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 27812	. . . . . . . . 9 |- { t | E. k e. [_ l / j ]_ B t = <. l , k >. } = ( { l } X. [_ l / j ]_ B )
137		esumeq1 28467	. . . . . . . . 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 2459	. . . . . . 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 2443	. . . . . 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 463	. . . . 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 6295	. . . 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 1728	. . . . . 6 |- F/ j ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
144		nfcv 2564	. . . . . 6 |- F/_ j b
145		nfcv 2564	. . . . . 6 |- F/_ j { l }
146		vex 3061	. . . . . . 7 |- b e. _V
147	146	a1i 11	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> b e. _V )
148		snex 4631	. . . . . . 7 |- { l } e. _V
149	148	a1i 11	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> { l } e. _V )
150	36	eldifbd 3426	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> -. l e. b )
151		disjsn 4031	. . . . . . 7 |- ( ( b i^i { l } ) = (/) <-> -. l e. b )
152	150, 151	sylibr 212	. . . . . 6 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( b i^i { l } ) = (/) )
153		simpll 752	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ph )
154		simprl 756	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> b C_ A )
155	154	sselda 3441	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j e. A )
156	47	anassrs 646	. . . . . . . . 9 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
157	156	ralrimiva 2817	. . . . . . . 8 |- ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) )
158		nfcv 2564	. . . . . . . . 9 |- F/_ k B
159	158	esumcl 28463	. . . . . . . 8 |- ( ( B e. W /\ A. k e. B C e. ( 0 [,] +oo ) ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
160	39, 157, 159	syl2anc 659	. . . . . . 7 |- ( ( ph /\ j e. A ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
161	153, 155, 160	syl2anc 659	. . . . . 6 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> Σ* k e. B C e. ( 0 [,] +oo ) )
162		simpll 752	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> ph )
163	55	snss 4095	. . . . . . . . 9 |- ( l e. A <-> { l } C_ A )
164	38, 163	sylib 196	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> { l } C_ A )
165	164	sselda 3441	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. { l } ) -> j e. A )
166	162, 165, 160	syl2anc 659	. . . . . 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 28486	. . . . 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 463	. . . 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 4355	. . . . . . . 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 4849	. . . . . . . . . . 11 |- F/_ j ( { l } X. [_ l / j ]_ B )
171		sneq 3981	. . . . . . . . . . . 12 |- ( j = l -> { j } = { l } )
172	171, 32	xpeq12d 4847	. . . . . . . . . . 11 |- ( j = l -> ( { j } X. B ) = ( { l } X. [_ l / j ]_ B ) )
173	170, 172	iunxsngf 27840	. . . . . . . . . 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 3593	. . . . . . . 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 2431	. . . . . . 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 28467	. . . . . . 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 1728	. . . . . . 7 |- F/ z ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) )
180		nfcv 2564	. . . . . . 7 |- F/_ z U_ j e. b ( { j } X. B )
181		nfcv 2564	. . . . . . 7 |- F/_ z ( { l } X. [_ l / j ]_ B )
182		snex 4631	. . . . . . . . . 10 |- { j } e. _V
183	155, 40	syldan 468	. . . . . . . . . 10 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> B e. W )
184		xpexg 6583	. . . . . . . . . 10 |- ( ( { j } e. _V /\ B e. W ) -> ( { j } X. B ) e. _V )
185	182, 183, 184	sylancr 661	. . . . . . . . 9 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> ( { j } X. B ) e. _V )
186	185	ralrimiva 2817	. . . . . . . 8 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> A. j e. b ( { j } X. B ) e. _V )
187		iunexg 6759	. . . . . . . 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 659	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> U_ j e. b ( { j } X. B ) e. _V )
189		xpexg 6583	. . . . . . . 8 |- ( ( { l } e. _V /\ [_ l / j ]_ B e. W ) -> ( { l } X. [_ l / j ]_ B ) e. _V )
190	148, 43, 189	sylancr 661	. . . . . . 7 |- ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( { l } X. [_ l / j ]_ B ) e. _V )
191		simpr 459	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j e. b )
192	150	adantr 463	. . . . . . . . . . . 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 659	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ j e. b ) -> j =/= l )
195		disjsn2 4032	. . . . . . . . . . 11 |- ( j =/= l -> ( { j } i^i { l } ) = (/) )
196		xpdisj1 5245	. . . . . . . . . . 11 |- ( ( { j } i^i { l } ) = (/) -> ( ( { j } X. B ) i^i ( { l } X. [_ l / j ]_ B ) ) = (/) )
197	194, 195, 196	3syl 20	. . . . . . . . . 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 2817	. . . . . . . . 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 4287	. . . . . . . . 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 27839	. . . . . . . 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 4326	. . . . . . . 8 |- U_ j e. b (/) = (/)
203	200, 201, 202	3eqtr3g 2466	. . . . . . 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 752	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> ph )
205		iunss1 4282	. . . . . . . . . 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 3441	. . . . . . . 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 1728	. . . . . . . . . 10 |- F/ j ph
209		nfcv 2564	. . . . . . . . . . 11 |- F/_ j z
210		nfiu1 4300	. . . . . . . . . . 11 |- F/_ j U_ j e. A ( { j } X. B )
211	209, 210	nfel 2577	. . . . . . . . . 10 |- F/ j z e. U_ j e. A ( { j } X. B )
212	208, 211	nfan 1956	. . . . . . . . 9 |- F/ j ( ph /\ z e. U_ j e. A ( { j } X. B ) )
213		nfv 1728	. . . . . . . . . 10 |- F/ k ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) )
214		nfcv 2564	. . . . . . . . . . 11 |- F/_ k ( 0 [,] +oo )
215	66, 214	nfel 2577	. . . . . . . . . 10 |- F/ k F e. ( 0 [,] +oo )
216	75	adantl 464	. . . . . . . . . . 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 770	. . . . . . . . . . . 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 769	. . . . . . . . . . . 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 754	. . . . . . . . . . . 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 1228	. . . . . . . . . . 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 2490	. . . . . . . . . 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 27892	. . . . . . . . . . . 12 |- ( j e. A -> ( z e. ( { j } X. B ) <-> E. k e. B z = <. j , k >. ) )
223	222	biimpa 482	. . . . . . . . . . 11 |- ( ( j e. A /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. )
224	223	adantll 712	. . . . . . . . . 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 2944	. . . . . . . . 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 459	. . . . . . . . . 10 |- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> z e. U_ j e. A ( { j } X. B ) )
227		eliun 4275	. . . . . . . . . 10 |- ( z e. U_ j e. A ( { j } X. B ) <-> E. j e. A z e. ( { j } X. B ) )
228	226, 227	sylib 196	. . . . . . . . 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 2946	. . . . . . . 8 |- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
230	204, 207, 229	syl2anc 659	. . . . . . 7 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. U_ j e. b ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
231		simpll 752	. . . . . . . 8 |- ( ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) /\ z e. ( { l } X. [_ l / j ]_ B ) ) -> ph )
232		nfcv 2564	. . . . . . . . . . 11 |- F/_ j A
233		nfcv 2564	. . . . . . . . . . 11 |- F/_ j l
234	232, 233, 170, 172	ssiun2sf 27842	. . . . . . . . . 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 3441	. . . . . . . 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 659	. . . . . . 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 28486	. . . . . 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 2455	. . . . 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 463	. . . 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 2453	. . 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 432	. 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 7795	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 184   /\ wa 367   = wceq 1405   e. wcel 1842   {cab 2387   F/_wnfc 2550   =/= wne 2598   A.wral 2753   E.wrex 2754   E!wreu 2755   _Vcvv 3058   [.wsbc 3276   [_csb 3372   \ cdif 3410   u. cun 3411   i^i cin 3412   C_ wss 3413   (/)c0 3737   {csn 3971   <.cop 3977   U_ciun 4270   |-> cmpt 4452   X. cxp 4820   `'ccnv 4821   Fun wfun 5562   ` cfv 5568  (class class class)co 6277   1stc1st 6781   2ndc2nd 6782   Fincfn 7553   0cc0 9521   +oocpnf 9654   +ecxad 11368   [,]cicc 11584  Σ^*cesum 28460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-inf2 8090  ax-cnex 9577  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-mulcom 9585  ax-addass 9586  ax-mulass 9587  ax-distr 9588  ax-i2m1 9589  ax-1ne0 9590  ax-1rid 9591  ax-rnegex 9592  ax-rrecex 9593  ax-cnre 9594  ax-pre-lttri 9595  ax-pre-lttrn 9596  ax-pre-ltadd 9597  ax-pre-mulgt0 9598  ax-pre-sup 9599  ax-addf 9600  ax-mulf 9601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-iin 4273  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-isom 5577  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6520  df-om 6683  df-1st 6783  df-2nd 6784  df-supp 6902  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-1o 7166  df-2o 7167  df-oadd 7170  df-er 7347  df-map 7458  df-pm 7459  df-ixp 7507  df-en 7554  df-dom 7555  df-sdom 7556  df-fin 7557  df-fsupp 7863  df-fi 7904  df-sup 7934  df-oi 7968  df-card 8351  df-cda 8579  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-sub 9842  df-neg 9843  df-div 10247  df-nn 10576  df-2 10634  df-3 10635  df-4 10636  df-5 10637  df-6 10638  df-7 10639  df-8 10640  df-9 10641  df-10 10642  df-n0 10836  df-z 10905  df-dec 11019  df-uz 11127  df-q 11227  df-rp 11265  df-xneg 11370  df-xadd 11371  df-xmul 11372  df-ioo 11585  df-ioc 11586  df-ico 11587  df-icc 11588  df-fz 11725  df-fzo 11853  df-fl 11964  df-mod 12033  df-seq 12150  df-exp 12209  df-fac 12396  df-bc 12423  df-hash 12451  df-shft 13047  df-cj 13079  df-re 13080  df-im 13081  df-sqrt 13215  df-abs 13216  df-limsup 13441  df-clim 13458  df-rlim 13459  df-sum 13656  df-ef 14010  df-sin 14012  df-cos 14013  df-pi 14015  df-struct 14841  df-ndx 14842  df-slot 14843  df-base 14844  df-sets 14845  df-ress 14846  df-plusg 14920  df-mulr 14921  df-starv 14922  df-sca 14923  df-vsca 14924  df-ip 14925  df-tset 14926  df-ple 14927  df-ds 14929  df-unif 14930  df-hom 14931  df-cco 14932  df-rest 15035  df-topn 15036  df-0g 15054  df-gsum 15055  df-topgen 15056  df-pt 15057  df-prds 15060  df-ordt 15113  df-xrs 15114  df-qtop 15119  df-imas 15120  df-xps 15122  df-mre 15198  df-mrc 15199  df-acs 15201  df-ps 16152  df-tsr 16153  df-plusf 16193  df-mgm 16194  df-sgrp 16233  df-mnd 16243  df-mhm 16288  df-submnd 16289  df-grp 16379  df-minusg 16380  df-sbg 16381  df-mulg 16382  df-subg 16520  df-cntz 16677  df-cmn 17122  df-abl 17123  df-mgp 17460  df-ur 17472  df-ring 17518  df-cring 17519  df-subrg 17745  df-abv 17784  df-lmod 17832  df-scaf 17833  df-sra 18136  df-rgmod 18137  df-psmet 18729  df-xmet 18730  df-met 18731  df-bl 18732  df-mopn 18733  df-fbas 18734  df-fg 18735  df-cnfld 18739  df-top 19689  df-bases 19691  df-topon 19692  df-topsp 19693  df-cld 19810  df-ntr 19811  df-cls 19812  df-nei 19890  df-lp 19928  df-perf 19929  df-cn 20019  df-cnp 20020  df-haus 20107  df-tx 20353  df-hmeo 20546  df-fil 20637  df-fm 20729  df-flim 20730  df-flf 20731  df-tmd 20861  df-tgp 20862  df-tsms 20915  df-trg 20952  df-xms 21113  df-ms 21114  df-tms 21115  df-nm 21393  df-ngp 21394  df-nrg 21396  df-nlm 21397  df-ii 21671  df-cncf 21672  df-limc 22560  df-dv 22561  df-log 23234  df-esum 28461

This theorem is referenced by:  esum2d  28526