Theorem prdsbnd2

Description: If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Hypotheses	prdsbnd.y	|- Y = ( S Xs_ R )
	prdsbnd.b	|- B = ( Base ` Y )
	prdsbnd.v	|- V = ( Base ` ( R ` x ) )
	prdsbnd.e	|- E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )
	prdsbnd.d	|- D = ( dist ` Y )
	prdsbnd.s	|- ( ph -> S e. W )
	prdsbnd.i	|- ( ph -> I e. Fin )
	prdsbnd.r	|- ( ph -> R Fn I )
	prdsbnd2.c	|- C = ( D |` ( A X. A ) )
	prdsbnd2.e	|- ( ( ph /\ x e. I ) -> E e. ( Met ` V ) )
	prdsbnd2.m	|- ( ( ph /\ x e. I ) -> ( ( E |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( E |` ( y X. y ) ) e. ( Bnd ` y ) ) )
Assertion	prdsbnd2	|- ( ph -> ( C e. ( TotBnd ` A ) <-> C e. ( Bnd ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbnd.y	|- Y = ( S Xs_ R )
2		prdsbnd.b	|- B = ( Base ` Y )
3		prdsbnd.v	|- V = ( Base ` ( R ` x ) )
4		prdsbnd.e	|- E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )
5		prdsbnd.d	|- D = ( dist ` Y )
6		prdsbnd.s	|- ( ph -> S e. W )
7		prdsbnd.i	|- ( ph -> I e. Fin )
8		prdsbnd.r	|- ( ph -> R Fn I )
9		prdsbnd2.c	|- C = ( D |` ( A X. A ) )
10		prdsbnd2.e	|- ( ( ph /\ x e. I ) -> E e. ( Met ` V ) )
11		prdsbnd2.m	|- ( ( ph /\ x e. I ) -> ( ( E |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( E |` ( y X. y ) ) e. ( Bnd ` y ) ) )
12		totbndbnd	|- ( C e. ( TotBnd ` A ) -> C e. ( Bnd ` A ) )
13		bndmet	|- ( C e. ( Bnd ` A ) -> C e. ( Met ` A ) )
14		0totbnd	|- ( A = (/) -> ( C e. ( TotBnd ` A ) <-> C e. ( Met ` A ) ) )
15	13 14	imbitrrid	|- ( A = (/) -> ( C e. ( Bnd ` A ) -> C e. ( TotBnd ` A ) ) )
16	15	a1i	|- ( ph -> ( A = (/) -> ( C e. ( Bnd ` A ) -> C e. ( TotBnd ` A ) ) ) )
17		n0	|- ( A =/= (/) <-> E. a a e. A )
18		simprr	|- ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) -> C e. ( Bnd ` A ) )
19		eqid	|- ( S Xs_ ( x e. I |-> ( R ` x ) ) ) = ( S Xs_ ( x e. I |-> ( R ` x ) ) )
20		eqid	|- ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) = ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
21		eqid	|- ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) = ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
22		fvexd	|- ( ( ph /\ x e. I ) -> ( R ` x ) e. _V )
23	19 20 3 4 21 6 7 22 10	prdsmet	|- ( ph -> ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) e. ( Met ` ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) ) )
24		dffn5	|- ( R Fn I <-> R = ( x e. I |-> ( R ` x ) ) )
25	8 24	sylib	|- ( ph -> R = ( x e. I |-> ( R ` x ) ) )
26	25	oveq2d	|- ( ph -> ( S Xs_ R ) = ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
27	1 26	eqtrid	|- ( ph -> Y = ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
28	27	fveq2d	|- ( ph -> ( dist ` Y ) = ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
29	5 28	eqtrid	|- ( ph -> D = ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
30	27	fveq2d	|- ( ph -> ( Base ` Y ) = ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
31	2 30	eqtrid	|- ( ph -> B = ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
32	31	fveq2d	|- ( ph -> ( Met ` B ) = ( Met ` ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) ) )
33	23 29 32	3eltr4d	|- ( ph -> D e. ( Met ` B ) )
34	33	adantr	|- ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) -> D e. ( Met ` B ) )
35		simpr	|- ( ( a e. A /\ C e. ( Bnd ` A ) ) -> C e. ( Bnd ` A ) )
36	9	bnd2lem	|- ( ( D e. ( Met ` B ) /\ C e. ( Bnd ` A ) ) -> A C_ B )
37	33 35 36	syl2an	|- ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) -> A C_ B )
38		simprl	|- ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) -> a e. A )
39	37 38	sseldd	|- ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) -> a e. B )
40	9	ssbnd	|- ( ( D e. ( Met ` B ) /\ a e. B ) -> ( C e. ( Bnd ` A ) <-> E. r e. RR A C_ ( a ( ball ` D ) r ) ) )
41	34 39 40	syl2anc	|- ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) -> ( C e. ( Bnd ` A ) <-> E. r e. RR A C_ ( a ( ball ` D ) r ) ) )
42	18 41	mpbid	|- ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) -> E. r e. RR A C_ ( a ( ball ` D ) r ) )
43		simprr	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> A C_ ( a ( ball ` D ) r ) )
44		xpss12	|- ( ( A C_ ( a ( ball ` D ) r ) /\ A C_ ( a ( ball ` D ) r ) ) -> ( A X. A ) C_ ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) )
45	43 43 44	syl2anc	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> ( A X. A ) C_ ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) )
46	45	resabs1d	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> ( ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) |` ( A X. A ) ) = ( D |` ( A X. A ) ) )
47	46 9	eqtr4di	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> ( ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) |` ( A X. A ) ) = C )
48		simpll	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> ph )
49	39	adantr	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> a e. B )
50		simprl	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> r e. RR )
51	38	adantr	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> a e. A )
52	43 51	sseldd	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> a e. ( a ( ball ` D ) r ) )
53	52	ne0d	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> ( a ( ball ` D ) r ) =/= (/) )
54	33	ad2antrr	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> D e. ( Met ` B ) )
55		metxmet	|- ( D e. ( Met ` B ) -> D e. ( *Met ` B ) )
56	54 55	syl	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> D e. ( *Met ` B ) )
57	50	rexrd	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> r e. RR* )
58		xbln0	|- ( ( D e. ( *Met ` B ) /\ a e. B /\ r e. RR* ) -> ( ( a ( ball ` D ) r ) =/= (/) <-> 0 < r ) )
59	56 49 57 58	syl3anc	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> ( ( a ( ball ` D ) r ) =/= (/) <-> 0 < r ) )
60	53 59	mpbid	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> 0 < r )
61	50 60	elrpd	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> r e. RR+ )
62		eqid	|- ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) = ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) )
63		eqid	|- ( Base ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) = ( Base ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) )
64		eqid	|- ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) = ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) )
65		eqid	|- ( ( dist ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) |` ( ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) X. ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) ) ) = ( ( dist ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) |` ( ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) X. ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) ) )
66		eqid	|- ( dist ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) = ( dist ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) )
67	6	adantr	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> S e. W )
68	7	adantr	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> I e. Fin )
69		ovex	|- ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) e. _V
70		fveq2	|- ( y = x -> ( R ` y ) = ( R ` x ) )
71		2fveq3	|- ( y = x -> ( dist ` ( R ` y ) ) = ( dist ` ( R ` x ) ) )
72		2fveq3	|- ( y = x -> ( Base ` ( R ` y ) ) = ( Base ` ( R ` x ) ) )
73	72 3	eqtr4di	|- ( y = x -> ( Base ` ( R ` y ) ) = V )
74	73	sqxpeqd	|- ( y = x -> ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) = ( V X. V ) )
75	71 74	reseq12d	|- ( y = x -> ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) = ( ( dist ` ( R ` x ) ) |` ( V X. V ) ) )
76	75 4	eqtr4di	|- ( y = x -> ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) = E )
77	76	fveq2d	|- ( y = x -> ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) = ( ball ` E ) )
78		fveq2	|- ( y = x -> ( a ` y ) = ( a ` x ) )
79		eqidd	|- ( y = x -> r = r )
80	77 78 79	oveq123d	|- ( y = x -> ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) = ( ( a ` x ) ( ball ` E ) r ) )
81	70 80	oveq12d	|- ( y = x -> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) = ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) )
82	81	cbvmptv	|- ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) = ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) )
83	69 82	fnmpti	|- ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) Fn I
84	83	a1i	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) Fn I )
85	10	adantlr	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> E e. ( Met ` V ) )
86		metxmet	|- ( E e. ( Met ` V ) -> E e. ( *Met ` V ) )
87	85 86	syl	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> E e. ( *Met ` V ) )
88	22	ralrimiva	|- ( ph -> A. x e. I ( R ` x ) e. _V )
89	88	adantr	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> A. x e. I ( R ` x ) e. _V )
90		simprl	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> a e. B )
91	31	adantr	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> B = ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
92	90 91	eleqtrd	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> a e. ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
93	19 20 67 68 89 3 92	prdsbascl	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> A. x e. I ( a ` x ) e. V )
94	93	r19.21bi	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( a ` x ) e. V )
95		simplrr	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> r e. RR+ )
96	95	rpred	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> r e. RR )
97		blbnd	|- ( ( E e. ( *Met ` V ) /\ ( a ` x ) e. V /\ r e. RR ) -> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( Bnd ` ( ( a ` x ) ( ball ` E ) r ) ) )
98	87 94 96 97	syl3anc	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( Bnd ` ( ( a ` x ) ( ball ` E ) r ) ) )
99		ovex	|- ( ( a ` x ) ( ball ` E ) r ) e. _V
100		xpeq12	|- ( ( y = ( ( a ` x ) ( ball ` E ) r ) /\ y = ( ( a ` x ) ( ball ` E ) r ) ) -> ( y X. y ) = ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) )
101	100	anidms	|- ( y = ( ( a ` x ) ( ball ` E ) r ) -> ( y X. y ) = ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) )
102	101	reseq2d	|- ( y = ( ( a ` x ) ( ball ` E ) r ) -> ( E |` ( y X. y ) ) = ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) )
103		fveq2	|- ( y = ( ( a ` x ) ( ball ` E ) r ) -> ( TotBnd ` y ) = ( TotBnd ` ( ( a ` x ) ( ball ` E ) r ) ) )
104	102 103	eleq12d	|- ( y = ( ( a ` x ) ( ball ` E ) r ) -> ( ( E |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( TotBnd ` ( ( a ` x ) ( ball ` E ) r ) ) ) )
105		fveq2	|- ( y = ( ( a ` x ) ( ball ` E ) r ) -> ( Bnd ` y ) = ( Bnd ` ( ( a ` x ) ( ball ` E ) r ) ) )
106	102 105	eleq12d	|- ( y = ( ( a ` x ) ( ball ` E ) r ) -> ( ( E |` ( y X. y ) ) e. ( Bnd ` y ) <-> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( Bnd ` ( ( a ` x ) ( ball ` E ) r ) ) ) )
107	104 106	bibi12d	|- ( y = ( ( a ` x ) ( ball ` E ) r ) -> ( ( ( E |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( E |` ( y X. y ) ) e. ( Bnd ` y ) ) <-> ( ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( TotBnd ` ( ( a ` x ) ( ball ` E ) r ) ) <-> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( Bnd ` ( ( a ` x ) ( ball ` E ) r ) ) ) ) )
108	107	imbi2d	|- ( y = ( ( a ` x ) ( ball ` E ) r ) -> ( ( ( ph /\ x e. I ) -> ( ( E |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( E |` ( y X. y ) ) e. ( Bnd ` y ) ) ) <-> ( ( ph /\ x e. I ) -> ( ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( TotBnd ` ( ( a ` x ) ( ball ` E ) r ) ) <-> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( Bnd ` ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) )
109	99 108 11	vtocl	|- ( ( ph /\ x e. I ) -> ( ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( TotBnd ` ( ( a ` x ) ( ball ` E ) r ) ) <-> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( Bnd ` ( ( a ` x ) ( ball ` E ) r ) ) ) )
110	109	adantlr	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( TotBnd ` ( ( a ` x ) ( ball ` E ) r ) ) <-> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( Bnd ` ( ( a ` x ) ( ball ` E ) r ) ) ) )
111	98 110	mpbird	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) e. ( TotBnd ` ( ( a ` x ) ( ball ` E ) r ) ) )
112		eqid	|- ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) = ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) )
113	81 112 69	fvmpt	|- ( x e. I -> ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) = ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) )
114	113	adantl	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) = ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) )
115	114	fveq2d	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( dist ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) = ( dist ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
116		eqid	|- ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) = ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) )
117		eqid	|- ( dist ` ( R ` x ) ) = ( dist ` ( R ` x ) )
118	116 117	ressds	|- ( ( ( a ` x ) ( ball ` E ) r ) e. _V -> ( dist ` ( R ` x ) ) = ( dist ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
119	99 118	ax-mp	|- ( dist ` ( R ` x ) ) = ( dist ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) )
120	115 119	eqtr4di	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( dist ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) = ( dist ` ( R ` x ) ) )
121	114	fveq2d	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) = ( Base ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
122		rpxr	|- ( r e. RR+ -> r e. RR* )
123	122	ad2antll	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> r e. RR* )
124	123	adantr	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> r e. RR* )
125		blssm	|- ( ( E e. ( *Met ` V ) /\ ( a ` x ) e. V /\ r e. RR* ) -> ( ( a ` x ) ( ball ` E ) r ) C_ V )
126	87 94 124 125	syl3anc	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( a ` x ) ( ball ` E ) r ) C_ V )
127	116 3	ressbas2	|- ( ( ( a ` x ) ( ball ` E ) r ) C_ V -> ( ( a ` x ) ( ball ` E ) r ) = ( Base ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
128	126 127	syl	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( a ` x ) ( ball ` E ) r ) = ( Base ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
129	121 128	eqtr4d	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) = ( ( a ` x ) ( ball ` E ) r ) )
130	129	sqxpeqd	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) X. ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) ) = ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) )
131	120 130	reseq12d	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( dist ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) |` ( ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) X. ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) ) ) = ( ( dist ` ( R ` x ) ) |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) )
132	4	reseq1i	|- ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) = ( ( ( dist ` ( R ` x ) ) |` ( V X. V ) ) |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) )
133		xpss12	|- ( ( ( ( a ` x ) ( ball ` E ) r ) C_ V /\ ( ( a ` x ) ( ball ` E ) r ) C_ V ) -> ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) C_ ( V X. V ) )
134	126 126 133	syl2anc	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) C_ ( V X. V ) )
135	134	resabs1d	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( ( dist ` ( R ` x ) ) |` ( V X. V ) ) |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) = ( ( dist ` ( R ` x ) ) |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) )
136	132 135	eqtrid	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) = ( ( dist ` ( R ` x ) ) |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) )
137	131 136	eqtr4d	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( dist ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) |` ( ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) X. ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) ) ) = ( E |` ( ( ( a ` x ) ( ball ` E ) r ) X. ( ( a ` x ) ( ball ` E ) r ) ) ) )
138	129	fveq2d	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( TotBnd ` ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) ) = ( TotBnd ` ( ( a ` x ) ( ball ` E ) r ) ) )
139	111 137 138	3eltr4d	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( dist ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) |` ( ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) X. ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) ) ) e. ( TotBnd ` ( Base ` ( ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ` x ) ) ) )
140	62 63 64 65 66 67 68 84 139	prdstotbnd	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( dist ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) e. ( TotBnd ` ( Base ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) ) )
141	27	adantr	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> Y = ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
142		eqidd	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) = ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) )
143		eqid	|- ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) = ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) )
144	82	oveq2i	|- ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) = ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
145	144	fveq2i	|- ( dist ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) = ( dist ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) )
146		fvexd	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( R ` x ) e. _V )
147	99	a1i	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( a ` x ) ( ball ` E ) r ) e. _V )
148	141 142 143 5 145 67 67 68 146 147	ressprdsds	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( dist ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) = ( D |` ( ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) X. ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) ) ) )
149	128	ixpeq2dva	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> X_ x e. I ( ( a ` x ) ( ball ` E ) r ) = X_ x e. I ( Base ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
150	70	cbvmptv	|- ( y e. I |-> ( R ` y ) ) = ( x e. I |-> ( R ` x ) )
151	150	oveq2i	|- ( S Xs_ ( y e. I |-> ( R ` y ) ) ) = ( S Xs_ ( x e. I |-> ( R ` x ) ) )
152	27 151	eqtr4di	|- ( ph -> Y = ( S Xs_ ( y e. I |-> ( R ` y ) ) ) )
153	152	fveq2d	|- ( ph -> ( dist ` Y ) = ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
154	5 153	eqtrid	|- ( ph -> D = ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
155	154	fveq2d	|- ( ph -> ( ball ` D ) = ( ball ` ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) ) )
156	155	oveqdr	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( a ( ball ` D ) r ) = ( a ( ball ` ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) ) r ) )
157		eqid	|- ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) = ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) )
158		eqid	|- ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) = ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) )
159	152	fveq2d	|- ( ph -> ( Base ` Y ) = ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
160	2 159	eqtrid	|- ( ph -> B = ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
161	160	adantr	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> B = ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
162	90 161	eleqtrd	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> a e. ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
163		rpgt0	|- ( r e. RR+ -> 0 < r )
164	163	ad2antll	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> 0 < r )
165	151 157 3 4 158 67 68 146 87 162 123 164	prdsbl	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( a ( ball ` ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) ) r ) = X_ x e. I ( ( a ` x ) ( ball ` E ) r ) )
166	156 165	eqtrd	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( a ( ball ` D ) r ) = X_ x e. I ( ( a ` x ) ( ball ` E ) r ) )
167		eqid	|- ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) = ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
168	69	a1i	|- ( ( ( ph /\ ( a e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) e. _V )
169	168	ralrimiva	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> A. x e. I ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) e. _V )
170		eqid	|- ( Base ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) = ( Base ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) )
171	167 143 67 68 169 170	prdsbas3	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) = X_ x e. I ( Base ` ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) )
172	149 166 171	3eqtr4rd	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) = ( a ( ball ` D ) r ) )
173	172	sqxpeqd	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) X. ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) ) = ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) )
174	173	reseq2d	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( D |` ( ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) X. ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) ) ) ) = ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) )
175	148 174	eqtrd	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( dist ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) = ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) )
176	144	fveq2i	|- ( Base ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) = ( Base ` ( S Xs_ ( x e. I |-> ( ( R ` x ) |`s ( ( a ` x ) ( ball ` E ) r ) ) ) ) )
177	176 172	eqtrid	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( Base ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) = ( a ( ball ` D ) r ) )
178	177	fveq2d	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( TotBnd ` ( Base ` ( S Xs_ ( y e. I |-> ( ( R ` y ) |`s ( ( a ` y ) ( ball ` ( ( dist ` ( R ` y ) ) |` ( ( Base ` ( R ` y ) ) X. ( Base ` ( R ` y ) ) ) ) ) r ) ) ) ) ) ) = ( TotBnd ` ( a ( ball ` D ) r ) ) )
179	140 175 178	3eltr3d	|- ( ( ph /\ ( a e. B /\ r e. RR+ ) ) -> ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) e. ( TotBnd ` ( a ( ball ` D ) r ) ) )
180	48 49 61 179	syl12anc	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) e. ( TotBnd ` ( a ( ball ` D ) r ) ) )
181		totbndss	|- ( ( ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) e. ( TotBnd ` ( a ( ball ` D ) r ) ) /\ A C_ ( a ( ball ` D ) r ) ) -> ( ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) |` ( A X. A ) ) e. ( TotBnd ` A ) )
182	180 43 181	syl2anc	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> ( ( D |` ( ( a ( ball ` D ) r ) X. ( a ( ball ` D ) r ) ) ) |` ( A X. A ) ) e. ( TotBnd ` A ) )
183	47 182	eqeltrrd	|- ( ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) /\ ( r e. RR /\ A C_ ( a ( ball ` D ) r ) ) ) -> C e. ( TotBnd ` A ) )
184	42 183	rexlimddv	|- ( ( ph /\ ( a e. A /\ C e. ( Bnd ` A ) ) ) -> C e. ( TotBnd ` A ) )
185	184	exp32	|- ( ph -> ( a e. A -> ( C e. ( Bnd ` A ) -> C e. ( TotBnd ` A ) ) ) )
186	185	exlimdv	|- ( ph -> ( E. a a e. A -> ( C e. ( Bnd ` A ) -> C e. ( TotBnd ` A ) ) ) )
187	17 186	biimtrid	|- ( ph -> ( A =/= (/) -> ( C e. ( Bnd ` A ) -> C e. ( TotBnd ` A ) ) ) )
188	16 187	pm2.61dne	|- ( ph -> ( C e. ( Bnd ` A ) -> C e. ( TotBnd ` A ) ) )
189	12 188	impbid2	|- ( ph -> ( C e. ( TotBnd ` A ) <-> C e. ( Bnd ` A ) ) )