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 ‘ 𝐶 ) )

Metamath Proof Explorer

Theorem equivcfil

Proof