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 β€˜ 𝐢 ) )