Theorem rrntotbnd 16846

Description: A set in Euclidean space is totally bounded iff its is bounded.

Hypotheses

Ref	Expression
rrntotbnd.1	|- X = (RR ^m (1...N))
rrntotbnd.2	|- M = ((RRn` N) |` (Y X. Y))

Assertion

Ref	Expression
rrntotbnd	|- ((N e. NN /\ Y C_ X) -> (M e. TotBnd <-> M e. Bnd))

Proof of Theorem rrntotbnd

Step	Hyp	Ref	Expression
1		eqid 2141	. . 3 |- dom dom M = dom dom M
2	1	totbndbnd 16768	. 2 |- (M e. TotBnd -> M e. Bnd)
3		rrntotbnd.2	. . . . . . . . 9 |- M = ((RRn` N) |` (Y X. Y))
4	3	a1i 8	. . . . . . . 8 |- ((N e. NN /\ Y C_ X) -> M = ((RRn` N) |` (Y X. Y)))
5	4	dmeqd 4285	. . . . . . 7 |- ((N e. NN /\ Y C_ X) -> dom M = dom ((RRn` N) |` (Y X. Y)))
6	5	dmeqd 4285	. . . . . 6 |- ((N e. NN /\ Y C_ X) -> dom dom M = dom dom ((RRn` N) |` (Y X. Y)))
7		rrnmet 16840	. . . . . . . 8 |- (N e. NN -> (RRn` N) e. Met)
8	7	adantr 447	. . . . . . 7 |- ((N e. NN /\ Y C_ X) -> (RRn` N) e. Met)
9		rrndm 16839	. . . . . . . . . 10 |- (N e. NN -> dom dom (RRn` N) = (RR ^m (1...N)))
10		rrntotbnd.1	. . . . . . . . . 10 |- X = (RR ^m (1...N))
11	9, 10	syl6eqr 2195	. . . . . . . . 9 |- (N e. NN -> dom dom (RRn` N) = X)
12	11	sseq2d 2872	. . . . . . . 8 |- (N e. NN -> (Y C_ dom dom (RRn` N) <-> Y C_ X))
13	12	biimpar 616	. . . . . . 7 |- ((N e. NN /\ Y C_ X) -> Y C_ dom dom (RRn` N))
14		eqid 2141	. . . . . . . 8 |- dom dom (RRn` N) = dom dom (RRn` N)
15	14	metssba2 9953	. . . . . . 7 |- (((RRn` N) e. Met /\ Y C_ dom dom (RRn` N)) -> Y = dom dom ((RRn` N) |` (Y X. Y)))
16	8, 13, 15	syl11anc 659	. . . . . 6 |- ((N e. NN /\ Y C_ X) -> Y = dom dom ((RRn` N) |` (Y X. Y)))
17	6, 16	eqtr4d 2176	. . . . 5 |- ((N e. NN /\ Y C_ X) -> dom dom M = Y)
18	17	raleqdv 2515	. . . 4 |- ((N e. NN /\ Y C_ X) -> (A.x e. dom dom ME.r e. RR+ dom dom M = (x( ball ` M)r) <-> A.x e. Y E.r e. RR+ dom dom M = (x( ball ` M)r)))
19		0fin 5839	. . . . . . . . 9 |- (/) e. Fin
20		id 15	. . . . . . . . . . . 12 |- (Y = (/) -> Y = (/))
21		0ss 3107	. . . . . . . . . . . . 13 |- (/) C_ U.(/)
22	21	a1i 8	. . . . . . . . . . . 12 |- (Y = (/) -> (/) C_ U.(/))
23	20, 22	eqsstrd 2878	. . . . . . . . . . 11 |- (Y = (/) -> Y C_ U.(/))
24	23	adantl 448	. . . . . . . . . 10 |- (((N e. NN /\ Y C_ X) /\ Y = (/)) -> Y C_ U.(/))
25		ral0 3173	. . . . . . . . . 10 |- A.b e. (/) E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d)
26	24, 25	jctir 502	. . . . . . . . 9 |- (((N e. NN /\ Y C_ X) /\ Y = (/)) -> (Y C_ U.(/) /\ A.b e. (/) E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d)))
27		unieq 3375	. . . . . . . . . . . 12 |- (v = (/) -> U.v = U.(/))
28	27	sseq2d 2872	. . . . . . . . . . 11 |- (v = (/) -> (Y C_ U.v <-> Y C_ U.(/)))
29		raleq 2511	. . . . . . . . . . 11 |- (v = (/) -> (A.b e. v E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d) <-> A.b e. (/) E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d)))
30	28, 29	anbi12d 763	. . . . . . . . . 10 |- (v = (/) -> ((Y C_ U.v /\ A.b e. v E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d)) <-> (Y C_ U.(/) /\ A.b e. (/) E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d))))
31	30	rcla4ev 2620	. . . . . . . . 9 |- (((/) e. Fin /\ (Y C_ U.(/) /\ A.b e. (/) E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d))) -> E.v e. Fin (Y C_ U.v /\ A.b e. v E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d)))
32	19, 26, 31	sylancr 662	. . . . . . . 8 |- (((N e. NN /\ Y C_ X) /\ Y = (/)) -> E.v e. Fin (Y C_ U.v /\ A.b e. v E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d)))
33	32	adantr 447	. . . . . . 7 |- ((((N e. NN /\ Y C_ X) /\ Y = (/)) /\ d e. RR+) -> E.v e. Fin (Y C_ U.v /\ A.b e. v E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d)))
34	33	r19.21aiva 2426	. . . . . 6 |- (((N e. NN /\ Y C_ X) /\ Y = (/)) -> A.d e. RR+ E.v e. Fin (Y C_ U.v /\ A.b e. v E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d)))
35	34	a1d 18	. . . . 5 |- (((N e. NN /\ Y C_ X) /\ Y = (/)) -> (A.x e. Y E.r e. RR+ dom dom M = (x( ball ` M)r) -> A.d e. RR+ E.v e. Fin (Y C_ U.v /\ A.b e. v E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d))))
36		df-ne 2268	. . . . . 6 |- (Y =/= (/) <-> -. Y = (/))
37		r19.2z 3158	. . . . . . . 8 |- ((Y =/= (/) /\ A.x e. Y E.r e. RR+ dom dom M = (x( ball ` M)r)) -> E.x e. Y E.r e. RR+ dom dom M = (x( ball ` M)r))
38		ssel2 2847	. . . . . . . . . . . . . . . . . . . . 21 |- ((Y C_ X /\ x e. Y) -> x e. X)
39	38	anim1i 538	. . . . . . . . . . . . . . . . . . . 20 |- (((Y C_ X /\ x e. Y) /\ r e. RR+) -> (x e. X /\ r e. RR+))
40	39	anasss 631	. . . . . . . . . . . . . . . . . . 19 |- ((Y C_ X /\ (x e. Y /\ r e. RR+)) -> (x e. X /\ r e. RR+))
41	40	anim2i 539	. . . . . . . . . . . . . . . . . 18 |- ((N e. NN /\ (Y C_ X /\ (x e. Y /\ r e. RR+))) -> (N e. NN /\ (x e. X /\ r e. RR+)))
42	41	anassrs 632	. . . . . . . . . . . . . . . . 17 |- (((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) -> (N e. NN /\ (x e. X /\ r e. RR+)))
43	7	adantr 447	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((N e. NN /\ x e. X) -> (RRn` N) e. Met)
44	9, 10	syl6reqr 2196	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (N e. NN -> X = dom dom (RRn` N))
45	44	eleq2d 2211	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (N e. NN -> (x e. X <-> x e. dom dom (RRn` N)))
46	45	biimpa 615	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((N e. NN /\ x e. X) -> x e. dom dom (RRn` N))
47	43, 46	jca 494	. . . . . . . . . . . . . . . . . . . . . 22 |- ((N e. NN /\ x e. X) -> ((RRn` N) e. Met /\ x e. dom dom (RRn` N)))
48		rpregt0 7582	. . . . . . . . . . . . . . . . . . . . . 22 |- (r e. RR+ -> (r e. RR /\ 0 < r))
49	14	elbl 9981	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((RRn` N) e. Met /\ x e. dom dom (RRn` N)) /\ (r e. RR /\ 0 < r)) -> (y e. (x( ball ` (RRn` N))r) <-> (y e. dom dom (RRn` N) /\ (x(RRn` N)y) < r)))
50	47, 48, 49	syl2an 603	. . . . . . . . . . . . . . . . . . . . 21 |- (((N e. NN /\ x e. X) /\ r e. RR+) -> (y e. (x( ball ` (RRn` N))r) <-> (y e. dom dom (RRn` N) /\ (x(RRn` N)y) < r)))
51	50	adantrl 779	. . . . . . . . . . . . . . . . . . . 20 |- (((N e. NN /\ x e. X) /\ (d e. RR+ /\ r e. RR+)) -> (y e. (x( ball ` (RRn` N))r) <-> (y e. dom dom (RRn` N) /\ (x(RRn` N)y) < r)))
52	10, 3	rrntotbndlem1 16844	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((N e. NN /\ x e. X) /\ (d e. RR+ /\ r e. RR+)) /\ (y e. dom dom (RRn` N) /\ (x(RRn` N)y) < r)) -> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d) e. {a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))})
53	9	eleq2d 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (N e. NN -> (y e. dom dom (RRn` N) <-> y e. (RR ^m (1...N))))
54	53	biimpd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (N e. NN -> (y e. dom dom (RRn` N) -> y e. (RR ^m (1...N))))
55	54	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((N e. NN /\ x e. X) /\ d e. RR+) -> (y e. dom dom (RRn` N) -> y e. (RR ^m (1...N))))
56	55	imdistani 770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((N e. NN /\ x e. X) /\ d e. RR+) /\ y e. dom dom (RRn` N)) -> (((N e. NN /\ x e. X) /\ d e. RR+) /\ y e. (RR ^m (1...N))))
57	10	eleq2i 2208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. X <-> x e. (RR ^m (1...N)))
58	57	biimpi 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. X -> x e. (RR ^m (1...N)))
59	58	anim2i 539	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((N e. NN /\ x e. X) -> (N e. NN /\ x e. (RR ^m (1...N))))
60	10, 3	rrntotbndlem2 16845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} (RRn` N)y) < d)
61	7	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> (RRn` N) e. Met)
62		reex 6816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- RR e. _V
63		oprex 5003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (1...N) e. _V
64	62, 63	elmap 5554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (x e. (RR ^m (1...N)) <-> x:(1...N)-->RR)
65		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((x:(1...N)-->RR /\ m e. (1...N)) -> (x` m) e. RR)
66	64, 65	sylanb 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((x e. (RR ^m (1...N)) /\ m e. (1...N)) -> (x` m) e. RR)
67	66	adantll 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((N e. NN /\ d e. RR+) /\ x e. (RR ^m (1...N))) /\ m e. (1...N)) -> (x` m) e. RR)
68	67	adantlrr 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ m e. (1...N)) -> (x` m) e. RR)
69		nnrp 7578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (N e. NN -> N e. RR+)
70		rpsqrcl 8349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (N e. RR+ -> (sqr` N) e. RR+)
71	69, 70	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (N e. NN -> (sqr` N) e. RR+)
72		rpdivcl 7589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((d e. RR+ /\ (sqr` N) e. RR+) -> (d / (sqr` N)) e. RR+)
73	71, 72	sylan2 600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((d e. RR+ /\ N e. NN) -> (d / (sqr` N)) e. RR+)
74		rpre 7576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((d / (sqr` N)) e. RR+ -> (d / (sqr` N)) e. RR)
75	73, 74	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((d e. RR+ /\ N e. NN) -> (d / (sqr` N)) e. RR)
76	75	ancoms 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((N e. NN /\ d e. RR+) -> (d / (sqr` N)) e. RR)
77	76	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ m e. (1...N)) -> (d / (sqr` N)) e. RR)
78	62, 63	elmap 5554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (y e. (RR ^m (1...N)) <-> y:(1...N)-->RR)
79		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((y:(1...N)-->RR /\ n e. (1...N)) -> (y` n) e. RR)
80	78, 79	sylanb 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((y e. (RR ^m (1...N)) /\ n e. (1...N)) -> (y` n) e. RR)
81	80	adantll 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (((x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N))) /\ n e. (1...N)) -> (y` n) e. RR)
82		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((x:(1...N)-->RR /\ n e. (1...N)) -> (x` n) e. RR)
83	64, 82	sylanb 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((x e. (RR ^m (1...N)) /\ n e. (1...N)) -> (x` n) e. RR)
84	83	adantlr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (((x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N))) /\ n e. (1...N)) -> (x` n) e. RR)
85		resubcl 7078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (((y` n) e. RR /\ (x` n) e. RR) -> ((y` n) - (x` n)) e. RR)
86	81, 84, 85	syl11anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (((x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N))) /\ n e. (1...N)) -> ((y` n) - (x` n)) e. RR)
87	86	adantll 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ n e. (1...N)) -> ((y` n) - (x` n)) e. RR)
88	76	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ n e. (1...N)) -> (d / (sqr` N)) e. RR)
89		rpne0 7583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((d / (sqr` N)) e. RR+ -> (d / (sqr` N)) =/= 0)
90	73, 89	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((d e. RR+ /\ N e. NN) -> (d / (sqr` N)) =/= 0)
91	90	ancoms 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((N e. NN /\ d e. RR+) -> (d / (sqr` N)) =/= 0)
92	91	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ n e. (1...N)) -> (d / (sqr` N)) =/= 0)
93		redivcl 7309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((y` n) - (x` n)) e. RR /\ (d / (sqr` N)) e. RR /\ (d / (sqr` N)) =/= 0) -> (((y` n) - (x` n)) / (d / (sqr` N))) e. RR)
94	87, 88, 92, 93	syl111anc 1349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ n e. (1...N)) -> (((y` n) - (x` n)) / (d / (sqr` N))) e. RR)
95		2re 7496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- 2 e. RR
96		2ne0 7507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- 2 =/= 0
97	95, 96	rereccli 7310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (1 / 2) e. RR
98		readdcl 6809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((((y` n) - (x` n)) / (d / (sqr` N))) e. RR /\ (1 / 2) e. RR) -> ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2)) e. RR)
99	94, 97, 98	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ n e. (1...N)) -> ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2)) e. RR)
100		flcl 7811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2)) e. RR -> (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))) e. ZZ)
101		zre 7689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))) e. ZZ -> (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))) e. RR)
102	99, 100, 101	3syl 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ n e. (1...N)) -> (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))) e. RR)
103	102	r19.21aiva 2426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> A.n e. (1...N)(|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))) e. RR)
104		eqid 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- {<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))} = {<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}
105	104	fopab2 4888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (A.n e. (1...N)(|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))) e. RR <-> {<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}:(1...N)-->RR)
106	103, 105	sylib 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> {<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}:(1...N)-->RR)
107		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}:(1...N)-->RR /\ m e. (1...N)) -> ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m) e. RR)
108	106, 107	sylan 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ m e. (1...N)) -> ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m) e. RR)
109		remulcl 6811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((d / (sqr` N)) e. RR /\ ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m) e. RR) -> ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m)) e. RR)
110	77, 108, 109	syl11anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ m e. (1...N)) -> ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m)) e. RR)
111		readdcl 6809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((x` m) e. RR /\ ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m)) e. RR) -> ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))) e. RR)
112	68, 110, 111	syl11anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) /\ m e. (1...N)) -> ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))) e. RR)
113	112	r19.21aiva 2426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> A.m e. (1...N)((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))) e. RR)
114		eqid 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} = {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))}
115	114	fopab2 4888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (A.m e. (1...N)((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))) e. RR <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))}:(1...N)-->RR)
116	113, 115	sylib 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))}:(1...N)-->RR)
117	9	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> dom dom (RRn` N) = (RR ^m (1...N)))
118	117	eleq2d 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} e. dom dom (RRn` N) <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} e. (RR ^m (1...N))))
119	62, 63	elmap 5554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} e. (RR ^m (1...N)) <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))}:(1...N)-->RR)
120	118, 119	syl6bb 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} e. dom dom (RRn` N) <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))}:(1...N)-->RR))
121	116, 120	mpbird 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} e. dom dom (RRn` N))
122	53	biimpar 616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((N e. NN /\ y e. (RR ^m (1...N))) -> y e. dom dom (RRn` N))
123	122	ad2ant2rl 809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> y e. dom dom (RRn` N))
124		rpregt0 7582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (d e. RR+ -> (d e. RR /\ 0 < d))
125	124	ad2antlr 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> (d e. RR /\ 0 < d))
126	14	elbl2 9982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((RRn` N) e. Met /\ {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} e. dom dom (RRn` N) /\ y e. dom dom (RRn` N)) /\ (d e. RR /\ 0 < d)) -> (y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d) <-> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} (RRn` N)y) < d))
127	61, 121, 123, 125, 126	syl31anc 1352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> (y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d) <-> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} (RRn` N)y) < d))
128	60, 127	mpbird 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((N e. NN /\ d e. RR+) /\ (x e. (RR ^m (1...N)) /\ y e. (RR ^m (1...N)))) -> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d))
129	128	expr 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((N e. NN /\ d e. RR+) /\ x e. (RR ^m (1...N))) -> (y e. (RR ^m (1...N)) -> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d)))
130	129	an32s 855	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((N e. NN /\ x e. (RR ^m (1...N))) /\ d e. RR+) -> (y e. (RR ^m (1...N)) -> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d)))
131	130	imp 393	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((N e. NN /\ x e. (RR ^m (1...N))) /\ d e. RR+) /\ y e. (RR ^m (1...N))) -> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d))
132	59, 131	sylanl1 641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((N e. NN /\ x e. X) /\ d e. RR+) /\ y e. (RR ^m (1...N))) -> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d))
133	56, 132	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((N e. NN /\ x e. X) /\ d e. RR+) /\ y e. dom dom (RRn` N)) -> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d))
134	133	adantlrr 789	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((N e. NN /\ x e. X) /\ (d e. RR+ /\ r e. RR+)) /\ y e. dom dom (RRn` N)) -> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d))
135	134	adantrr 781	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((N e. NN /\ x e. X) /\ (d e. RR+ /\ r e. RR+)) /\ (y e. dom dom (RRn` N) /\ (x(RRn` N)y) < r)) -> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d))
136		eleq2 2205	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d) -> (y e. z <-> y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d)))
137	136	rcla4ev 2620	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d) e. {a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))} /\ y e. ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. ({<.n, v>. | (n e. (1...N) /\ v = (|_` ((((y` n) - (x` n)) / (d / (sqr` N))) + (1 / 2))))}` m))))} ( ball ` (RRn` N))d)) -> E.z e. {a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}y e. z)
138	52, 135, 137	syl11anc 659	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((N e. NN /\ x e. X) /\ (d e. RR+ /\ r e. RR+)) /\ (y e. dom dom (RRn` N) /\ (x(RRn` N)y) < r)) -> E.z e. {a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}y e. z)
139		eluni2 3370	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))} <-> E.z e. {a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}y e. z)
140	138, 139	sylibr 243	. . . . . . . . . . . . . . . . . . . . 21 |- ((((N e. NN /\ x e. X) /\ (d e. RR+ /\ r e. RR+)) /\ (y e. dom dom (RRn` N) /\ (x(RRn` N)y) < r)) -> y e. U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))})
141	140	ex 398	. . . . . . . . . . . . . . . . . . . 20 |- (((N e. NN /\ x e. X) /\ (d e. RR+ /\ r e. RR+)) -> ((y e. dom dom (RRn` N) /\ (x(RRn` N)y) < r) -> y e. U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}))
142	51, 141	sylbid 246	. . . . . . . . . . . . . . . . . . 19 |- (((N e. NN /\ x e. X) /\ (d e. RR+ /\ r e. RR+)) -> (y e. (x( ball ` (RRn` N))r) -> y e. U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}))
143	142	an4s 884	. . . . . . . . . . . . . . . . . 18 |- (((N e. NN /\ d e. RR+) /\ (x e. X /\ r e. RR+)) -> (y e. (x( ball ` (RRn` N))r) -> y e. U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}))
144	143	an32s 855	. . . . . . . . . . . . . . . . 17 |- (((N e. NN /\ (x e. X /\ r e. RR+)) /\ d e. RR+) -> (y e. (x( ball ` (RRn` N))r) -> y e. U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}))
145	42, 144	sylan 597	. . . . . . . . . . . . . . . 16 |- ((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) -> (y e. (x( ball ` (RRn` N))r) -> y e. U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}))
146	145	ssrdv 2853	. . . . . . . . . . . . . . 15 |- ((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) -> (x( ball ` (RRn` N))r) C_ U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))})
147	16, 6	eqtr4d 2176	. . . . . . . . . . . . . . . . . . 19 |- ((N e. NN /\ Y C_ X) -> Y = dom dom M)
148	147	adantr 447	. . . . . . . . . . . . . . . . . 18 |- (((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) -> Y = dom dom M)
149	148	eqeq1d 2149	. . . . . . . . . . . . . . . . 17 |- (((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) -> (Y = (x( ball ` M)r) <-> dom dom M = (x( ball ` M)r)))
150	8, 13	jca 494	. . . . . . . . . . . . . . . . . . 19 |- ((N e. NN /\ Y C_ X) -> ((RRn` N) e. Met /\ Y C_ dom dom (RRn` N)))
151	14, 3	blssp 16668	. . . . . . . . . . . . . . . . . . . 20 |- ((((RRn` N) e. Met /\ Y C_ dom dom (RRn` N)) /\ (x e. Y /\ r e. RR+)) -> (x( ball ` M)r) = ((x( ball ` (RRn` N))r) i^i Y))
152		inss1 3026	. . . . . . . . . . . . . . . . . . . . 21 |- ((x( ball ` (RRn` N))r) i^i Y) C_ (x( ball ` (RRn` N))r)
153	152	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- ((((RRn` N) e. Met /\ Y C_ dom dom (RRn` N)) /\ (x e. Y /\ r e. RR+)) -> ((x( ball ` (RRn` N))r) i^i Y) C_ (x( ball ` (RRn` N))r))
154	151, 153	eqsstrd 2878	. . . . . . . . . . . . . . . . . . 19 |- ((((RRn` N) e. Met /\ Y C_ dom dom (RRn` N)) /\ (x e. Y /\ r e. RR+)) -> (x( ball ` M)r) C_ (x( ball ` (RRn` N))r))
155	150, 154	sylan 597	. . . . . . . . . . . . . . . . . 18 |- (((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) -> (x( ball ` M)r) C_ (x( ball ` (RRn` N))r))
156		sseq1 2865	. . . . . . . . . . . . . . . . . 18 |- (Y = (x( ball ` M)r) -> (Y C_ (x( ball ` (RRn` N))r) <-> (x( ball ` M)r) C_ (x( ball ` (RRn` N))r)))
157	155, 156	syl5ibrcom 258	. . . . . . . . . . . . . . . . 17 |- (((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) -> (Y = (x( ball ` M)r) -> Y C_ (x( ball ` (RRn` N))r)))
158	149, 157	sylbird 248	. . . . . . . . . . . . . . . 16 |- (((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) -> (dom dom M = (x( ball ` M)r) -> Y C_ (x( ball ` (RRn` N))r)))
159	158	adantr 447	. . . . . . . . . . . . . . 15 |- ((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) -> (dom dom M = (x( ball ` M)r) -> Y C_ (x( ball ` (RRn` N))r)))
160		sstr 2855	. . . . . . . . . . . . . . . 16 |- ((Y C_ (x( ball ` (RRn` N))r) /\ (x( ball ` (RRn` N))r) C_ U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}) -> Y C_ U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))})
161	160	expcom 399	. . . . . . . . . . . . . . 15 |- ((x( ball ` (RRn` N))r) C_ U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))} -> (Y C_ (x( ball ` (RRn` N))r) -> Y C_ U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}))
162	146, 159, 161	sylsyld 60	. . . . . . . . . . . . . 14 |- ((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) -> (dom dom M = (x( ball ` M)r) -> Y C_ U.{a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))}))
163		visset 2541	. . . . . . . . . . . . . . . . 17 |- b e. _V
164		eqeq1 2147	. . . . . . . . . . . . . . . . . . 19 |- (a = b -> (a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d) <-> b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d)))
165	164	anbi2d 751	. . . . . . . . . . . . . . . . . 18 |- (a = b -> ((f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d)) <-> (f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))))
166	165	exbidv 1926	. . . . . . . . . . . . . . . . 17 |- (a = b -> (E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d)) <-> E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))))
167	163, 166	elab 2644	. . . . . . . . . . . . . . . 16 |- (b e. {a | E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ a = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))} <-> E.f(f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d)))
168	57, 64	bitri 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x e. X <-> x:(1...N)-->RR)
169	168	biimpi 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x e. X -> x:(1...N)-->RR)
170	169	adantl 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((N e. NN /\ x e. X) -> x:(1...N)-->RR)
171	38, 170	sylan2 600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((N e. NN /\ (Y C_ X /\ x e. Y)) -> x:(1...N)-->RR)
172	171	anassrs 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((N e. NN /\ Y C_ X) /\ x e. Y) -> x:(1...N)-->RR)
173	172, 65	sylan 597	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((N e. NN /\ Y C_ X) /\ x e. Y) /\ m e. (1...N)) -> (x` m) e. RR)
174	173	adantlrr 789	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ m e. (1...N)) -> (x` m) e. RR)
175	174	ad2ant2rl 809	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ (f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ m e. (1...N))) -> (x` m) e. RR)
176	76	adantlr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((N e. NN /\ Y C_ X) /\ d e. RR+) -> (d / (sqr` N)) e. RR)
177	176	adantlr 777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) -> (d / (sqr` N)) e. RR)
178		fzssuz 8040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) C_ (ZZ>=` -u((|_` (r / (d / (sqr` N)))) + 1))
179		uzssz 7946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (ZZ>=` -u((|_` (r / (d / (sqr` N)))) + 1)) C_ ZZ
180	178, 179	sstri 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) C_ ZZ
181		zssre 7692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ZZ C_ RR
182	180, 181	sstri 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) C_ RR
183		fss 4667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ (-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) C_ RR) -> f:(1...N)-->RR)
184	182, 183	mpan2 679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) -> f:(1...N)-->RR)
185		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f:(1...N)-->RR /\ m e. (1...N)) -> (f` m) e. RR)
186	184, 185	sylan 597	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ m e. (1...N)) -> (f` m) e. RR)
187		remulcl 6811	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((d / (sqr` N)) e. RR /\ (f` m) e. RR) -> ((d / (sqr` N)) x. (f` m)) e. RR)
188	177, 186, 187	syl2an 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ (f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ m e. (1...N))) -> ((d / (sqr` N)) x. (f` m)) e. RR)
189		readdcl 6809	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((x` m) e. RR /\ ((d / (sqr` N)) x. (f` m)) e. RR) -> ((x` m) + ((d / (sqr` N)) x. (f` m))) e. RR)
190	175, 188, 189	syl11anc 659	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ (f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ m e. (1...N))) -> ((x` m) + ((d / (sqr` N)) x. (f` m))) e. RR)
191	190	anassrs 632	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1))) /\ m e. (1...N)) -> ((x` m) + ((d / (sqr` N)) x. (f` m))) e. RR)
192	191	r19.21aiva 2426	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1))) -> A.m e. (1...N)((x` m) + ((d / (sqr` N)) x. (f` m))) e. RR)
193		eqid 2141	. . . . . . . . . . . . . . . . . . . . . . 23 |- {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} = {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))}
194	193	fopab2 4888	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.m e. (1...N)((x` m) + ((d / (sqr` N)) x. (f` m))) e. RR <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))}:(1...N)-->RR)
195	192, 194	sylib 242	. . . . . . . . . . . . . . . . . . . . 21 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1))) -> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))}:(1...N)-->RR)
196	9	eleq2d 2211	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (N e. NN -> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. dom dom (RRn` N) <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. (RR ^m (1...N))))
197	62, 63	elmap 5554	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. (RR ^m (1...N)) <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))}:(1...N)-->RR)
198	196, 197	syl6bb 729	. . . . . . . . . . . . . . . . . . . . . . 23 |- (N e. NN -> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. dom dom (RRn` N) <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))}:(1...N)-->RR))
199	198	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . 22 |- (((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) -> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. dom dom (RRn` N) <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))}:(1...N)-->RR))
200	199	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . 21 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1))) -> ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. dom dom (RRn` N) <-> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))}:(1...N)-->RR))
201	195, 200	mpbird 318	. . . . . . . . . . . . . . . . . . . 20 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1))) -> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. dom dom (RRn` N))
202	201	adantrr 781	. . . . . . . . . . . . . . . . . . 19 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ (f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))) -> {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. dom dom (RRn` N))
203		simprr 813	. . . . . . . . . . . . . . . . . . 19 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ (f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))) -> b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))
204		opreq1 4986	. . . . . . . . . . . . . . . . . . . . 21 |- (y = {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} -> (y( ball ` (RRn` N))d) = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))
205	204	eqeq2d 2152	. . . . . . . . . . . . . . . . . . . 20 |- (y = {<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} -> (b = (y( ball ` (RRn` N))d) <-> b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d)))
206	205	rcla4ev 2620	. . . . . . . . . . . . . . . . . . 19 |- (({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} e. dom dom (RRn` N) /\ b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d)) -> E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d))
207	202, 203, 206	syl11anc 659	. . . . . . . . . . . . . . . . . 18 |- (((((N e. NN /\ Y C_ X) /\ (x e. Y /\ r e. RR+)) /\ d e. RR+) /\ (f:(1...N)-->(-u((|_` (r / (d / (sqr` N)))) + 1)...((|_` (r / (d / (sqr` N)))) + 1)) /\ b = ({<.m, u>. | (m e. (1...N) /\ u = ((x` m) + ((d / (sqr` N)) x. (f` m))))} ( ball ` (RRn` N))d))) -> E.y e. dom dom (RRn` N)b = (y( ball ` (RRn` N))d))
208	207