This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )