Metamath Proof Explorer


Theorem prdsbl

Description: A ball in the product metric for finite index set is the Cartesian product of balls in all coordinates. For infinite index set this is no longer true; instead the correct statement is that a *closed ball* is the product of closed balls in each coordinate (where closed ball means a set of the form in blcld ) - for a counterexample the point p in RR ^ NN whose n -th coordinate is 1 - 1 / n is in X_ n e. NN ball ( 0 , 1 ) but is not in the 1 -ball of the product (since d ( 0 , p ) = 1 ).

The last assumption, 0 < A , is needed only in the case I = (/) , when the right side evaluates to { (/) } and the left evaluates to (/) if A <_ 0 and { (/) } if 0 < A . (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses prdsbl.y 𝑌 = ( 𝑆 Xs ( 𝑥𝐼𝑅 ) )
prdsbl.b 𝐵 = ( Base ‘ 𝑌 )
prdsbl.v 𝑉 = ( Base ‘ 𝑅 )
prdsbl.e 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
prdsbl.d 𝐷 = ( dist ‘ 𝑌 )
prdsbl.s ( 𝜑𝑆𝑊 )
prdsbl.i ( 𝜑𝐼 ∈ Fin )
prdsbl.r ( ( 𝜑𝑥𝐼 ) → 𝑅𝑍 )
prdsbl.m ( ( 𝜑𝑥𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
prdsbl.p ( 𝜑𝑃𝐵 )
prdsbl.a ( 𝜑𝐴 ∈ ℝ* )
prdsbl.g ( 𝜑 → 0 < 𝐴 )
Assertion prdsbl ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝐴 ) = X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) )

Proof

Step Hyp Ref Expression
1 prdsbl.y 𝑌 = ( 𝑆 Xs ( 𝑥𝐼𝑅 ) )
2 prdsbl.b 𝐵 = ( Base ‘ 𝑌 )
3 prdsbl.v 𝑉 = ( Base ‘ 𝑅 )
4 prdsbl.e 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
5 prdsbl.d 𝐷 = ( dist ‘ 𝑌 )
6 prdsbl.s ( 𝜑𝑆𝑊 )
7 prdsbl.i ( 𝜑𝐼 ∈ Fin )
8 prdsbl.r ( ( 𝜑𝑥𝐼 ) → 𝑅𝑍 )
9 prdsbl.m ( ( 𝜑𝑥𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
10 prdsbl.p ( 𝜑𝑃𝐵 )
11 prdsbl.a ( 𝜑𝐴 ∈ ℝ* )
12 prdsbl.g ( 𝜑 → 0 < 𝐴 )
13 8 ralrimiva ( 𝜑 → ∀ 𝑥𝐼 𝑅𝑍 )
14 1 2 6 7 13 3 prdsbas3 ( 𝜑𝐵 = X 𝑥𝐼 𝑉 )
15 14 eleq2d ( 𝜑 → ( 𝑓𝐵𝑓X 𝑥𝐼 𝑉 ) )
16 15 biimpa ( ( 𝜑𝑓𝐵 ) → 𝑓X 𝑥𝐼 𝑉 )
17 ixpfn ( 𝑓X 𝑥𝐼 𝑉𝑓 Fn 𝐼 )
18 vex 𝑓 ∈ V
19 18 elixp ( 𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ↔ ( 𝑓 Fn 𝐼 ∧ ∀ 𝑥𝐼 ( 𝑓𝑥 ) ∈ ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ) )
20 19 baib ( 𝑓 Fn 𝐼 → ( 𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ↔ ∀ 𝑥𝐼 ( 𝑓𝑥 ) ∈ ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ) )
21 16 17 20 3syl ( ( 𝜑𝑓𝐵 ) → ( 𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ↔ ∀ 𝑥𝐼 ( 𝑓𝑥 ) ∈ ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ) )
22 9 adantlr ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
23 11 ad2antrr ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → 𝐴 ∈ ℝ* )
24 1 2 6 7 13 3 10 prdsbascl ( 𝜑 → ∀ 𝑥𝐼 ( 𝑃𝑥 ) ∈ 𝑉 )
25 24 adantr ( ( 𝜑𝑓𝐵 ) → ∀ 𝑥𝐼 ( 𝑃𝑥 ) ∈ 𝑉 )
26 25 r19.21bi ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( 𝑃𝑥 ) ∈ 𝑉 )
27 6 adantr ( ( 𝜑𝑓𝐵 ) → 𝑆𝑊 )
28 7 adantr ( ( 𝜑𝑓𝐵 ) → 𝐼 ∈ Fin )
29 13 adantr ( ( 𝜑𝑓𝐵 ) → ∀ 𝑥𝐼 𝑅𝑍 )
30 simpr ( ( 𝜑𝑓𝐵 ) → 𝑓𝐵 )
31 1 2 27 28 29 3 30 prdsbascl ( ( 𝜑𝑓𝐵 ) → ∀ 𝑥𝐼 ( 𝑓𝑥 ) ∈ 𝑉 )
32 31 r19.21bi ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( 𝑓𝑥 ) ∈ 𝑉 )
33 elbl2 ( ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝐴 ∈ ℝ* ) ∧ ( ( 𝑃𝑥 ) ∈ 𝑉 ∧ ( 𝑓𝑥 ) ∈ 𝑉 ) ) → ( ( 𝑓𝑥 ) ∈ ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ↔ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
34 22 23 26 32 33 syl22anc ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( 𝑓𝑥 ) ∈ ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ↔ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
35 34 ralbidva ( ( 𝜑𝑓𝐵 ) → ( ∀ 𝑥𝐼 ( 𝑓𝑥 ) ∈ ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ↔ ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
36 xmetcl ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑃𝑥 ) ∈ 𝑉 ∧ ( 𝑓𝑥 ) ∈ 𝑉 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ ℝ* )
37 22 26 32 36 syl3anc ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ ℝ* )
38 37 ralrimiva ( ( 𝜑𝑓𝐵 ) → ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ ℝ* )
39 eqid ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) = ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) )
40 breq1 ( 𝑧 = ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) → ( 𝑧 < 𝐴 ↔ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
41 39 40 ralrnmptw ( ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ ℝ* → ( ∀ 𝑧 ∈ ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) 𝑧 < 𝐴 ↔ ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
42 38 41 syl ( ( 𝜑𝑓𝐵 ) → ( ∀ 𝑧 ∈ ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) 𝑧 < 𝐴 ↔ ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
43 12 adantr ( ( 𝜑𝑓𝐵 ) → 0 < 𝐴 )
44 c0ex 0 ∈ V
45 breq1 ( 𝑧 = 0 → ( 𝑧 < 𝐴 ↔ 0 < 𝐴 ) )
46 44 45 ralsn ( ∀ 𝑧 ∈ { 0 } 𝑧 < 𝐴 ↔ 0 < 𝐴 )
47 43 46 sylibr ( ( 𝜑𝑓𝐵 ) → ∀ 𝑧 ∈ { 0 } 𝑧 < 𝐴 )
48 ralunb ( ∀ 𝑧 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) 𝑧 < 𝐴 ↔ ( ∀ 𝑧 ∈ ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) 𝑧 < 𝐴 ∧ ∀ 𝑧 ∈ { 0 } 𝑧 < 𝐴 ) )
49 10 adantr ( ( 𝜑𝑓𝐵 ) → 𝑃𝐵 )
50 1 2 27 28 29 49 30 3 4 5 prdsdsval3 ( ( 𝜑𝑓𝐵 ) → ( 𝑃 𝐷 𝑓 ) = sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
51 xrltso < Or ℝ*
52 51 a1i ( ( 𝜑𝑓𝐵 ) → < Or ℝ* )
53 39 rnmpt ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) = { 𝑦 ∣ ∃ 𝑥𝐼 𝑦 = ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) }
54 abrexfi ( 𝐼 ∈ Fin → { 𝑦 ∣ ∃ 𝑥𝐼 𝑦 = ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) } ∈ Fin )
55 53 54 eqeltrid ( 𝐼 ∈ Fin → ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∈ Fin )
56 28 55 syl ( ( 𝜑𝑓𝐵 ) → ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∈ Fin )
57 snfi { 0 } ∈ Fin
58 unfi ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∈ Fin ∧ { 0 } ∈ Fin ) → ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ∈ Fin )
59 56 57 58 sylancl ( ( 𝜑𝑓𝐵 ) → ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ∈ Fin )
60 ssun2 { 0 } ⊆ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } )
61 44 snss ( 0 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ↔ { 0 } ⊆ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) )
62 60 61 mpbir 0 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } )
63 ne0i ( 0 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) → ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ≠ ∅ )
64 62 63 mp1i ( ( 𝜑𝑓𝐵 ) → ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ≠ ∅ )
65 37 fmpttd ( ( 𝜑𝑓𝐵 ) → ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) : 𝐼 ⟶ ℝ* )
66 65 frnd ( ( 𝜑𝑓𝐵 ) → ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ⊆ ℝ* )
67 0xr 0 ∈ ℝ*
68 67 a1i ( ( 𝜑𝑓𝐵 ) → 0 ∈ ℝ* )
69 68 snssd ( ( 𝜑𝑓𝐵 ) → { 0 } ⊆ ℝ* )
70 66 69 unssd ( ( 𝜑𝑓𝐵 ) → ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
71 fisupcl ( ( < Or ℝ* ∧ ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ∈ Fin ∧ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ≠ ∅ ∧ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* ) ) → sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) )
72 52 59 64 70 71 syl13anc ( ( 𝜑𝑓𝐵 ) → sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) )
73 50 72 eqeltrd ( ( 𝜑𝑓𝐵 ) → ( 𝑃 𝐷 𝑓 ) ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) )
74 breq1 ( 𝑧 = ( 𝑃 𝐷 𝑓 ) → ( 𝑧 < 𝐴 ↔ ( 𝑃 𝐷 𝑓 ) < 𝐴 ) )
75 74 rspcv ( ( 𝑃 𝐷 𝑓 ) ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) → ( ∀ 𝑧 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) 𝑧 < 𝐴 → ( 𝑃 𝐷 𝑓 ) < 𝐴 ) )
76 73 75 syl ( ( 𝜑𝑓𝐵 ) → ( ∀ 𝑧 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) 𝑧 < 𝐴 → ( 𝑃 𝐷 𝑓 ) < 𝐴 ) )
77 48 76 syl5bir ( ( 𝜑𝑓𝐵 ) → ( ( ∀ 𝑧 ∈ ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) 𝑧 < 𝐴 ∧ ∀ 𝑧 ∈ { 0 } 𝑧 < 𝐴 ) → ( 𝑃 𝐷 𝑓 ) < 𝐴 ) )
78 47 77 mpan2d ( ( 𝜑𝑓𝐵 ) → ( ∀ 𝑧 ∈ ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) 𝑧 < 𝐴 → ( 𝑃 𝐷 𝑓 ) < 𝐴 ) )
79 42 78 sylbird ( ( 𝜑𝑓𝐵 ) → ( ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 → ( 𝑃 𝐷 𝑓 ) < 𝐴 ) )
80 ssun1 ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ⊆ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } )
81 ovex ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ V
82 81 elabrex ( 𝑥𝐼 → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ { 𝑦 ∣ ∃ 𝑥𝐼 𝑦 = ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) } )
83 82 adantl ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ { 𝑦 ∣ ∃ 𝑥𝐼 𝑦 = ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) } )
84 83 53 eleqtrrdi ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) )
85 80 84 sselid ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) )
86 supxrub ( ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* ∧ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ≤ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
87 70 85 86 syl2an2r ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ≤ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
88 50 adantr ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( 𝑃 𝐷 𝑓 ) = sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
89 87 88 breqtrrd ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ≤ ( 𝑃 𝐷 𝑓 ) )
90 1 2 3 4 5 6 7 8 9 prdsxmet ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
91 90 ad2antrr ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
92 10 ad2antrr ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → 𝑃𝐵 )
93 30 adantr ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → 𝑓𝐵 )
94 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑃𝐵𝑓𝐵 ) → ( 𝑃 𝐷 𝑓 ) ∈ ℝ* )
95 91 92 93 94 syl3anc ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( 𝑃 𝐷 𝑓 ) ∈ ℝ* )
96 xrlelttr ( ( ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ∈ ℝ* ∧ ( 𝑃 𝐷 𝑓 ) ∈ ℝ*𝐴 ∈ ℝ* ) → ( ( ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ≤ ( 𝑃 𝐷 𝑓 ) ∧ ( 𝑃 𝐷 𝑓 ) < 𝐴 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
97 37 95 23 96 syl3anc ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) ≤ ( 𝑃 𝐷 𝑓 ) ∧ ( 𝑃 𝐷 𝑓 ) < 𝐴 ) → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
98 89 97 mpand ( ( ( 𝜑𝑓𝐵 ) ∧ 𝑥𝐼 ) → ( ( 𝑃 𝐷 𝑓 ) < 𝐴 → ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
99 98 ralrimdva ( ( 𝜑𝑓𝐵 ) → ( ( 𝑃 𝐷 𝑓 ) < 𝐴 → ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ) )
100 79 99 impbid ( ( 𝜑𝑓𝐵 ) → ( ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) 𝐸 ( 𝑓𝑥 ) ) < 𝐴 ↔ ( 𝑃 𝐷 𝑓 ) < 𝐴 ) )
101 21 35 100 3bitrrd ( ( 𝜑𝑓𝐵 ) → ( ( 𝑃 𝐷 𝑓 ) < 𝐴𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ) )
102 101 pm5.32da ( 𝜑 → ( ( 𝑓𝐵 ∧ ( 𝑃 𝐷 𝑓 ) < 𝐴 ) ↔ ( 𝑓𝐵𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ) ) )
103 elbl ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑃𝐵𝐴 ∈ ℝ* ) → ( 𝑓 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝐴 ) ↔ ( 𝑓𝐵 ∧ ( 𝑃 𝐷 𝑓 ) < 𝐴 ) ) )
104 90 10 11 103 syl3anc ( 𝜑 → ( 𝑓 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝐴 ) ↔ ( 𝑓𝐵 ∧ ( 𝑃 𝐷 𝑓 ) < 𝐴 ) ) )
105 24 r19.21bi ( ( 𝜑𝑥𝐼 ) → ( 𝑃𝑥 ) ∈ 𝑉 )
106 11 adantr ( ( 𝜑𝑥𝐼 ) → 𝐴 ∈ ℝ* )
107 blssm ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑃𝑥 ) ∈ 𝑉𝐴 ∈ ℝ* ) → ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ⊆ 𝑉 )
108 9 105 106 107 syl3anc ( ( 𝜑𝑥𝐼 ) → ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ⊆ 𝑉 )
109 108 ralrimiva ( 𝜑 → ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ⊆ 𝑉 )
110 ss2ixp ( ∀ 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ⊆ 𝑉X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ⊆ X 𝑥𝐼 𝑉 )
111 109 110 syl ( 𝜑X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ⊆ X 𝑥𝐼 𝑉 )
112 111 14 sseqtrrd ( 𝜑X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ⊆ 𝐵 )
113 112 sseld ( 𝜑 → ( 𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) → 𝑓𝐵 ) )
114 113 pm4.71rd ( 𝜑 → ( 𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ↔ ( 𝑓𝐵𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ) ) )
115 102 104 114 3bitr4d ( 𝜑 → ( 𝑓 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝐴 ) ↔ 𝑓X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) ) )
116 115 eqrdv ( 𝜑 → ( 𝑃 ( ball ‘ 𝐷 ) 𝐴 ) = X 𝑥𝐼 ( ( 𝑃𝑥 ) ( ball ‘ 𝐸 ) 𝐴 ) )