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 | sseldi | ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑃 ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ( 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 ‘ 𝐸 ) 𝐴 ) ) |