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 ‘ 𝐸 ) 𝐴 ) ) |
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 ‘ 𝐸 ) 𝐴 ) ) |