Metamath Proof Explorer

Theorem equivcfil

Description: If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y ) ), all the D -Cauchy filters are also C -Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses equivcau.1 ⊢ ( 𝜑 → 𝐶 ∈ ( Met ‘ 𝑋 ) )
equivcau.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
equivcau.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
equivcau.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
Assertion equivcfil ( 𝜑 → ( CauFil ‘ 𝐷 ) ⊆ ( CauFil ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 equivcau.1 ⊢ ( 𝜑 → 𝐶 ∈ ( Met ‘ 𝑋 ) )
2 equivcau.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 equivcau.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
4 equivcau.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
5 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
6 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑅 ∈ ℝ+ )
7 5 6 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 𝑅 ) ∈ ℝ+ )
8 oveq2 ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) )
9 8 eleq1d ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 ↔ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 ) )
10 9 rexbidv ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 ) )
11 10 rspcv ⊢ ( ( 𝑟 / 𝑅 ) ∈ ℝ+ → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 ) )
12 7 11 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 ) )
13 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
14 eqid ⊢ ( MetOpen ‘ 𝐶 ) = ( MetOpen ‘ 𝐶 )
15 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
16 14 15 1 2 3 4 metss2lem ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
17 16 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
18 17 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
19 18 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
20 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ( Met ‘ 𝑋 ) )
21 metxmet ⊢ ( 𝐶 ∈ ( Met ‘ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
22 20 21 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
23 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
24 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
25 24 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝑟 ∈ ℝ* )
26 blssm ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑋 )
27 22 23 25 26 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑋 )
28 filss ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 )
29 28 3exp2 ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 → ( ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑋 → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) ) ) )
30 29 com24 ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑋 → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) ) ) )
31 13 19 27 30 syl3c ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) )
32 31 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ∈ 𝑓 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) )
33 12 32 syld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) )
34 33 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) )
35 34 imdistanda ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 ) → ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) ) )
36 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
37 iscfil3 ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 ) ) )
38 2 36 37 3syl ⊢ ( 𝜑 → ( 𝑓 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ∈ 𝑓 ) ) )
39 iscfil3 ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( CauFil ‘ 𝐶 ) ↔ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) ) )
40 1 21 39 3syl ⊢ ( 𝜑 → ( 𝑓 ∈ ( CauFil ‘ 𝐶 ) ↔ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ 𝑓 ) ) )
41 35 38 40 3imtr4d ⊢ ( 𝜑 → ( 𝑓 ∈ ( CauFil ‘ 𝐷 ) → 𝑓 ∈ ( CauFil ‘ 𝐶 ) ) )
42 41 ssrdv ⊢ ( 𝜑 → ( CauFil ‘ 𝐷 ) ⊆ ( CauFil ‘ 𝐶 ) )