Theorem fsumcnlem 7986

Description: Lemma for fsumcn 7987. Warning: The HTML proof page is 0.4MB in size.

Hypotheses

Ref	Expression
fsumcn.1	|- C e. Met
fsumcn.2	|- X = dom dom C
fsumcn.7	|- D = (abs o. - )
fsumcn.j	|- J = (Open` C)
fsumcn.k	|- K = (Open` D)
fsumcn.11	|- (k e. NN -> F e. (J Cn K))
fsumcn.13	|- G = {<.w, v>. | (w e. X /\ v = sum_k e. (1...N)(F` w))}
fsumcnlem.14	|- B = {<.<.u, t>., s>. | ((u e. (CC X. CC) /\ t e. (CC X. CC)) /\ s = sup({((1st` u)D(1st` t)), ((2nd` u)D(2nd` t))}, RR, < ))}

Assertion

Ref	Expression
fsumcnlem	|- (N e. NN -> G e. (J Cn K))

Distinct variable groups:   w,C   t,s,u,w,D   v,s,F,t,u,w   v,N,w   w,k,J   k,K,w   k,s,t,u,v,X,w

Proof of Theorem fsumcnlem

Step	Hyp	Ref	Expression
1		elnnuz 6441	. . . . . . . . . . . 12 |- (m e. NN <-> m e. (ZZ>` 1))
2		fvex 3738	. . . . . . . . . . . . 13 |- (F` w) e. V
3	2	fsump1slem 7012	. . . . . . . . . . . 12 |- (m e. (ZZ>` 1) -> sum_k e. (1...(m + 1))(F` w) = (sum_k e. (1...m)(F` w) + [_(m + 1) / k]_(F` w)))
4	1, 3	sylbi 199	. . . . . . . . . . 11 |- (m e. NN -> sum_k e. (1...(m + 1))(F` w) = (sum_k e. (1...m)(F` w) + [_(m + 1) / k]_(F` w)))
5	4	adantr 391	. . . . . . . . . 10 |- ((m e. NN /\ w e. X) -> sum_k e. (1...(m + 1))(F` w) = (sum_k e. (1...m)(F` w) + [_(m + 1) / k]_(F` w)))
6		sumex 6981	. . . . . . . . . . . . 13 |- sum_k e. (1...m)(F` w) e. V
7		fvopab2 3797	. . . . . . . . . . . . 13 |- ((w e. X /\ sum_k e. (1...m)(F` w) e. V) -> ({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) = sum_k e. (1...m)(F` w))
8	6, 7	mpan2 698	. . . . . . . . . . . 12 |- (w e. X -> ({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) = sum_k e. (1...m)(F` w))
9		oprex 3989	. . . . . . . . . . . . . . 15 |- (m + 1) e. V
10		csbfv12g 3748	. . . . . . . . . . . . . . 15 |- ((m + 1) e. V -> [_(m + 1) / k]_(F` w) = ([_(m + 1) / k]_F` [_(m + 1) / k]_w))
11	9, 10	ax-mp 7	. . . . . . . . . . . . . 14 |- [_(m + 1) / k]_(F` w) = ([_(m + 1) / k]_F` [_(m + 1) / k]_w)
12		ax-17 973	. . . . . . . . . . . . . . . . 17 |- (v e. w -> A.k v e. w)
13	12	csbconstgf 2013	. . . . . . . . . . . . . . . 16 |- ((m + 1) e. V -> [_(m + 1) / k]_w = w)
14	9, 13	ax-mp 7	. . . . . . . . . . . . . . 15 |- [_(m + 1) / k]_w = w
15	14	fveq2i 3733	. . . . . . . . . . . . . 14 |- ([_(m + 1) / k]_F` [_(m + 1) / k]_w) = ([_(m + 1) / k]_F` w)
16	11, 15	eqtr2 1499	. . . . . . . . . . . . 13 |- ([_(m + 1) / k]_F` w) = [_(m + 1) / k]_(F` w)
17	16	a1i 8	. . . . . . . . . . . 12 |- (w e. X -> ([_(m + 1) / k]_F` w) = [_(m + 1) / k]_(F` w))
18	8, 17	opreq12d 3984	. . . . . . . . . . 11 |- (w e. X -> (({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) + ([_(m + 1) / k]_F` w)) = (sum_k e. (1...m)(F` w) + [_(m + 1) / k]_(F` w)))
19	18	adantl 390	. . . . . . . . . 10 |- ((m e. NN /\ w e. X) -> (({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) + ([_(m + 1) / k]_F` w)) = (sum_k e. (1...m)(F` w) + [_(m + 1) / k]_(F` w)))
20	5, 19	eqtr4d 1513	. . . . . . . . 9 |- ((m e. NN /\ w e. X) -> sum_k e. (1...(m + 1))(F` w) = (({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) + ([_(m + 1) / k]_F` w)))
21	20	eqeq2d 1489	. . . . . . . 8 |- ((m e. NN /\ w e. X) -> (v = sum_k e. (1...(m + 1))(F` w) <-> v = (({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) + ([_(m + 1) / k]_F` w))))
22	21	pm5.32da 651	. . . . . . 7 |- (m e. NN -> ((w e. X /\ v = sum_k e. (1...(m + 1))(F` w)) <-> (w e. X /\ v = (({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) + ([_(m + 1) / k]_F` w)))))
23	22	opabbidv 2675	. . . . . 6 |- (m e. NN -> {<.w, v>. | (w e. X /\ v = sum_k e. (1...(m + 1))(F` w))} = {<.w, v>. | (w e. X /\ v = (({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) + ([_(m + 1) / k]_F` w)))})
24	23	adantr 391	. . . . 5 |- ((m e. NN /\ {<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))} e. (J Cn K)) -> {<.w, v>. | (w e. X /\ v = sum_k e. (1...(m + 1))(F` w))} = {<.w, v>. | (w e. X /\ v = (({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) + ([_(m + 1) / k]_F` w)))})
25		fsumcn.2	. . . . . . . 8 |- X = dom dom C
26		fsumcn.7	. . . . . . . . 9 |- D = (abs o. - )
27	26	cnmetba 7900	. . . . . . . 8 |- CC = dom dom D
28		fsumcn.1	. . . . . . . 8 |- C e. Met
29	26	cnmet 7901	. . . . . . . 8 |- D e. Met
30		fsumcn.j	. . . . . . . 8 |- J = (Open` C)
31		fsumcn.k	. . . . . . . 8 |- K = (Open` D)
32		eqid 1478	. . . . . . . 8 |- (Open` B) = (Open` B)
33		fsumcnlem.14	. . . . . . . 8 |- B = {<.<.u, t>., s>. | ((u e. (CC X. CC) /\ t e. (CC X. CC)) /\ s = sup({((1st` u)D(1st` t)), ((2nd` u)D(2nd` t))}, RR, < ))}
34	26, 33, 31, 32	addcn 7983	. . . . . . . 8 |- + e. ((Open` B) Cn K)
35		eleq1 1537	. . . . . . . . . . . . . . . 16 |- (w = r -> (w e. X <-> r e. X))
36	35	adantr 391	. . . . . . . . . . . . . . 15 |- ((w = r /\ v = q) -> (w e. X <-> r e. X))
37		id 59	. . . . . . . . . . . . . . . 16 |- (v = q -> v = q)
38		fveq2 3730	. . . . . . . . . . . . . . . . 17 |- (w = r -> (F` w) = (F` r))
39	38	sumeq2sdv 6993	. . . . . . . . . . . . . . . 16 |- (w = r -> sum_k e. (1...m)(F` w) = sum_k e. (1...m)(F` r))
40	37, 39	eqeqan12rd 1494	. . . . . . . . . . . . . . 15 |- ((w = r /\ v = q) -> (v = sum_k e. (1...m)(F` w) <-> q = sum_k e. (1...m)(F` r)))
41	36, 40	anbi12d 630	. . . . . . . . . . . . . 14 |- ((w = r /\ v = q) -> ((w e. X /\ v = sum_k e. (1...m)(F` w)) <-> (r e. X /\ q = sum_k e. (1...m)(F` r))))
42	41	cbvopabv 2678	. . . . . . . . . . . . 13 |- {<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))} = {<.r, q>. | (r e. X /\ q = sum_k e. (1...m)(F` r))}
43	42	fveq1i 3731	. . . . . . . . . . . 12 |- ({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) = ({<.r, q>. | (r e. X /\ q = sum_k e. (1...m)(F` r))}` w)
44	43	opreq1i 3977	. . . . . . . . . . 11 |- (({<.w, v>. | (w e. X /\ v = sum_k e. (1...m)(F` w))}` w) + ([_(m + 1) / k]_F` w)) = (({<.r, q>. | (r e. X /\ q = sum_k e. (1...m)(F` r))}` w) + ([_(m + 1) / k]_F` w))
45	44	eqeq2i 1488	. . . . . . . . . 10 |- (v = (({<.w, v>. | (w e. X /\ v = sum_k e. (1...