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

Metamath Proof Explorer

Theorem imasf1omet

Description: The image of a metric is a metric. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses imasf1oxmet.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasf1oxmet.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasf1oxmet.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
imasf1oxmet.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
imasf1oxmet.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
imasf1oxmet.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
imasf1omet.m ⊢ ( 𝜑 → 𝐸 ∈ ( Met ‘ 𝑉 ) )
Assertion imasf1omet ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 imasf1oxmet.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasf1oxmet.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasf1oxmet.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4 imasf1oxmet.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 imasf1oxmet.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
6 imasf1oxmet.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
7 imasf1omet.m ⊢ ( 𝜑 → 𝐸 ∈ ( Met ‘ 𝑉 ) )
8 metxmet ⊢ ( 𝐸 ∈ ( Met ‘ 𝑉 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
9 7 8 syl ⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
10 1 2 3 4 5 6 9 imasf1oxmet ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
11 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –onto→ 𝐵 )
12 3 11 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
13 eqid ⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
14 1 2 12 4 13 6 imasdsfn ⊢ ( 𝜑 → 𝐷 Fn ( 𝐵 × 𝐵 ) )
15 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑈 = ( 𝐹 “s 𝑅 ) )
16 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
17 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
18 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑅 ∈ 𝑍 )
19 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
20 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 ∈ 𝑉 )
21 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑏 ∈ 𝑉 )
22 15 16 17 18 5 6 19 20 21 imasdsf1o ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐸 𝑏 ) )
23 metcl ⊢ ( ( 𝐸 ∈ ( Met ‘ 𝑉 ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ )
24 23 3expb ⊢ ( ( 𝐸 ∈ ( Met ‘ 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ )
25 7 24 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ )
26 22 25 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ )
27 26 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ )
28 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 Fn 𝑉 )
29 3 28 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
30 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) )
31 30 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ) )
32 31 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ) )
33 29 32 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ) )
34 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
35 12 34 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
36 35 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
37 33 36 bitr3d ⊢ ( 𝜑 → ( ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
38 37 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
39 27 38 mpbid ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ )
40 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( 𝑥 𝐷 𝑦 ) = ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) )
41 40 eleq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
42 41 ralbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
43 42 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
44 29 43 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ) )
45 35 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
46 44 45 bitr3d ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
47 39 46 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
48 ffnov ⊢ ( 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ ↔ ( 𝐷 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
49 14 47 48 sylanbrc ⊢ ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ )
50 ismet2 ⊢ ( 𝐷 ∈ ( Met ‘ 𝐵 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ ) )
51 10 49 50 sylanbrc ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )