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

Metamath Proof Explorer

Theorem metss2lem

Description: Lemma for metss2 . (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses metequiv.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metequiv.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
metss2.1 ⊢ ( 𝜑 → 𝐶 ∈ ( Met ‘ 𝑋 ) )
metss2.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
metss2.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
metss2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
Assertion metss2lem ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑆 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑆 ) )

Proof

Step Hyp Ref Expression
1 metequiv.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metequiv.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 metss2.1 ⊢ ( 𝜑 → 𝐶 ∈ ( Met ‘ 𝑋 ) )
4 metss2.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
5 metss2.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
6 metss2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
7 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
8 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
9 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
10 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
11 7 8 9 10 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
12 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑆 ∈ ℝ+ )
13 12 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑆 ∈ ℝ )
14 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑅 ∈ ℝ+ )
15 11 13 14 ltmuldiv2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) < 𝑆 ↔ ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) ) )
16 6 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
17 16 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
18 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝐶 ∈ ( Met ‘ 𝑋 ) )
19 metcl ⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ )
20 18 8 9 19 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ )
21 14 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑅 ∈ ℝ )
22 21 11 remulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) ∈ ℝ )
23 lelttr ⊢ ( ( ( 𝑥 𝐶 𝑦 ) ∈ ℝ ∧ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( ( ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) ∧ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) < 𝑆 ) → ( 𝑥 𝐶 𝑦 ) < 𝑆 ) )
24 20 22 13 23 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) ∧ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) < 𝑆 ) → ( 𝑥 𝐶 𝑦 ) < 𝑆 ) )
25 17 24 mpand ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) < 𝑆 → ( 𝑥 𝐶 𝑦 ) < 𝑆 ) )
26 15 25 sylbird ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) → ( 𝑥 𝐶 𝑦 ) < 𝑆 ) )
27 26 ss2rabdv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) } ⊆ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐶 𝑦 ) < 𝑆 } )
28 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
29 4 28 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
31 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → 𝑥 ∈ 𝑋 )
32 simpr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) → 𝑆 ∈ ℝ+ )
33 rpdivcl ⊢ ( ( 𝑆 ∈ ℝ+ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑆 / 𝑅 ) ∈ ℝ+ )
34 32 5 33 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑆 / 𝑅 ) ∈ ℝ+ )
35 34 rpxrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑆 / 𝑅 ) ∈ ℝ* )
36 blval ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑆 / 𝑅 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑆 / 𝑅 ) ) = { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) } )
37 30 31 35 36 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑆 / 𝑅 ) ) = { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) } )
38 metxmet ⊢ ( 𝐶 ∈ ( Met ‘ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
39 3 38 syl ⊢ ( 𝜑 → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
41 rpxr ⊢ ( 𝑆 ∈ ℝ+ → 𝑆 ∈ ℝ* )
42 41 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → 𝑆 ∈ ℝ* )
43 blval ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑆 ) = { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐶 𝑦 ) < 𝑆 } )
44 40 31 42 43 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑆 ) = { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐶 𝑦 ) < 𝑆 } )
45 27 37 44 3sstr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑆 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑆 ) )