Metamath Proof Explorer

Theorem imasdsf1o

Description: The distance function is transferred across an image structure under a bijection. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses imasdsf1o.u ⊢ φ → U = F “ 𝑠 R
imasdsf1o.v ⊢ φ → V = Base R
imasdsf1o.f ⊢ φ → F : V ⟶ 1-1 onto B
imasdsf1o.r ⊢ φ → R ∈ Z
imasdsf1o.e ⊢ E = dist ⁡ R ↾ V × V
imasdsf1o.d ⊢ D = dist ⁡ U
imasdsf1o.m ⊢ φ → E ∈ ∞Met ⁡ V
imasdsf1o.x ⊢ φ → X ∈ V
imasdsf1o.y ⊢ φ → Y ∈ V
Assertion imasdsf1o ⊢ φ → F ⁡ X D F ⁡ Y = X E Y

Proof

Step Hyp Ref Expression
1 imasdsf1o.u ⊢ φ → U = F “ 𝑠 R
2 imasdsf1o.v ⊢ φ → V = Base R
3 imasdsf1o.f ⊢ φ → F : V ⟶ 1-1 onto B
4 imasdsf1o.r ⊢ φ → R ∈ Z
5 imasdsf1o.e ⊢ E = dist ⁡ R ↾ V × V
6 imasdsf1o.d ⊢ D = dist ⁡ U
7 imasdsf1o.m ⊢ φ → E ∈ ∞Met ⁡ V
8 imasdsf1o.x ⊢ φ → X ∈ V
9 imasdsf1o.y ⊢ φ → Y ∈ V
10 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ = ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
11 eqid ⊢ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = F ⁡ X ∧ F ⁡ 2 nd ⁡ h ⁡ n = F ⁡ Y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 = h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = F ⁡ X ∧ F ⁡ 2 nd ⁡ h ⁡ n = F ⁡ Y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1
12 eqid ⊢ ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = F ⁡ X ∧ F ⁡ 2 nd ⁡ h ⁡ n = F ⁡ Y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g = ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = F ⁡ X ∧ F ⁡ 2 nd ⁡ h ⁡ n = F ⁡ Y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g
13 1 2 3 4 5 6 7 8 9 10 11 12 imasdsf1olem ⊢ φ → F ⁡ X D F ⁡ Y = X E Y