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 ⊢ φ → U = F “ 𝑠 R
imasf1oxmet.v ⊢ φ → V = Base R
imasf1oxmet.f ⊢ φ → F : V ⟶ 1-1 onto B
imasf1oxmet.r ⊢ φ → R ∈ Z
imasf1oxmet.e ⊢ E = dist ⁡ R ↾ V × V
imasf1oxmet.d ⊢ D = dist ⁡ U
imasf1omet.m ⊢ φ → E ∈ Met ⁡ V
Assertion imasf1omet ⊢ φ → D ∈ Met ⁡ B

Proof

Step Hyp Ref Expression
1 imasf1oxmet.u ⊢ φ → U = F “ 𝑠 R
2 imasf1oxmet.v ⊢ φ → V = Base R
3 imasf1oxmet.f ⊢ φ → F : V ⟶ 1-1 onto B
4 imasf1oxmet.r ⊢ φ → R ∈ Z
5 imasf1oxmet.e ⊢ E = dist ⁡ R ↾ V × V
6 imasf1oxmet.d ⊢ D = dist ⁡ U
7 imasf1omet.m ⊢ φ → E ∈ Met ⁡ V
8 metxmet ⊢ E ∈ Met ⁡ V → E ∈ ∞Met ⁡ V
9 7 8 syl ⊢ φ → E ∈ ∞Met ⁡ V
10 1 2 3 4 5 6 9 imasf1oxmet ⊢ φ → D ∈ ∞Met ⁡ B
11 f1ofo ⊢ F : V ⟶ 1-1 onto B → F : V ⟶ onto B
12 3 11 syl ⊢ φ → F : V ⟶ onto B
13 eqid ⊢ dist ⁡ R = dist ⁡ R
14 1 2 12 4 13 6 imasdsfn ⊢ φ → D Fn B × B
15 1 adantr ⊢ φ ∧ a ∈ V ∧ b ∈ V → U = F “ 𝑠 R
16 2 adantr ⊢ φ ∧ a ∈ V ∧ b ∈ V → V = Base R
17 3 adantr ⊢ φ ∧ a ∈ V ∧ b ∈ V → F : V ⟶ 1-1 onto B
18 4 adantr ⊢ φ ∧ a ∈ V ∧ b ∈ V → R ∈ Z
19 9 adantr ⊢ φ ∧ a ∈ V ∧ b ∈ V → E ∈ ∞Met ⁡ V
20 simprl ⊢ φ ∧ a ∈ V ∧ b ∈ V → a ∈ V
21 simprr ⊢ φ ∧ a ∈ V ∧ b ∈ V → b ∈ V
22 15 16 17 18 5 6 19 20 21 imasdsf1o ⊢ φ ∧ a ∈ V ∧ b ∈ V → F ⁡ a D F ⁡ b = a E b
23 metcl ⊢ E ∈ Met ⁡ V ∧ a ∈ V ∧ b ∈ V → a E b ∈ ℝ
24 23 3expb ⊢ E ∈ Met ⁡ V ∧ a ∈ V ∧ b ∈ V → a E b ∈ ℝ
25 7 24 sylan ⊢ φ ∧ a ∈ V ∧ b ∈ V → a E b ∈ ℝ
26 22 25 eqeltrd ⊢ φ ∧ a ∈ V ∧ b ∈ V → F ⁡ a D F ⁡ b ∈ ℝ
27 26 ralrimivva ⊢ φ → ∀ a ∈ V ∀ b ∈ V F ⁡ a D F ⁡ b ∈ ℝ
28 f1ofn ⊢ F : V ⟶ 1-1 onto B → F Fn V
29 3 28 syl ⊢ φ → F Fn V
30 oveq2 ⊢ y = F ⁡ b → F ⁡ a D y = F ⁡ a D F ⁡ b
31 30 eleq1d ⊢ y = F ⁡ b → F ⁡ a D y ∈ ℝ ↔ F ⁡ a D F ⁡ b ∈ ℝ
32 31 ralrn ⊢ F Fn V → ∀ y ∈ ran ⁡ F F ⁡ a D y ∈ ℝ ↔ ∀ b ∈ V F ⁡ a D F ⁡ b ∈ ℝ
33 29 32 syl ⊢ φ → ∀ y ∈ ran ⁡ F F ⁡ a D y ∈ ℝ ↔ ∀ b ∈ V F ⁡ a D F ⁡ b ∈ ℝ
34 forn ⊢ F : V ⟶ onto B → ran ⁡ F = B
35 12 34 syl ⊢ φ → ran ⁡ F = B
36 35 raleqdv ⊢ φ → ∀ y ∈ ran ⁡ F F ⁡ a D y ∈ ℝ ↔ ∀ y ∈ B F ⁡ a D y ∈ ℝ
37 33 36 bitr3d ⊢ φ → ∀ b ∈ V F ⁡ a D F ⁡ b ∈ ℝ ↔ ∀ y ∈ B F ⁡ a D y ∈ ℝ
38 37 ralbidv ⊢ φ → ∀ a ∈ V ∀ b ∈ V F ⁡ a D F ⁡ b ∈ ℝ ↔ ∀ a ∈ V ∀ y ∈ B F ⁡ a D y ∈ ℝ
39 27 38 mpbid ⊢ φ → ∀ a ∈ V ∀ y ∈ B F ⁡ a D y ∈ ℝ
40 oveq1 ⊢ x = F ⁡ a → x D y = F ⁡ a D y
41 40 eleq1d ⊢ x = F ⁡ a → x D y ∈ ℝ ↔ F ⁡ a D y ∈ ℝ
42 41 ralbidv ⊢ x = F ⁡ a → ∀ y ∈ B x D y ∈ ℝ ↔ ∀ y ∈ B F ⁡ a D y ∈ ℝ
43 42 ralrn ⊢ F Fn V → ∀ x ∈ ran ⁡ F ∀ y ∈ B x D y ∈ ℝ ↔ ∀ a ∈ V ∀ y ∈ B F ⁡ a D y ∈ ℝ
44 29 43 syl ⊢ φ → ∀ x ∈ ran ⁡ F ∀ y ∈ B x D y ∈ ℝ ↔ ∀ a ∈ V ∀ y ∈ B F ⁡ a D y ∈ ℝ
45 35 raleqdv ⊢ φ → ∀ x ∈ ran ⁡ F ∀ y ∈ B x D y ∈ ℝ ↔ ∀ x ∈ B ∀ y ∈ B x D y ∈ ℝ
46 44 45 bitr3d ⊢ φ → ∀ a ∈ V ∀ y ∈ B F ⁡ a D y ∈ ℝ ↔ ∀ x ∈ B ∀ y ∈ B x D y ∈ ℝ
47 39 46 mpbid ⊢ φ → ∀ x ∈ B ∀ y ∈ B x D y ∈ ℝ
48 ffnov ⊢ D : B × B ⟶ ℝ ↔ D Fn B × B ∧ ∀ x ∈ B ∀ y ∈ B x D y ∈ ℝ
49 14 47 48 sylanbrc ⊢ φ → D : B × B ⟶ ℝ
50 ismet2 ⊢ D ∈ Met ⁡ B ↔ D ∈ ∞Met ⁡ B ∧ D : B × B ⟶ ℝ
51 10 49 50 sylanbrc ⊢ φ → D ∈ Met ⁡ B