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

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 ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasdsf1o.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasdsf1o.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
imasdsf1o.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
imasdsf1o.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
imasdsf1o.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
imasdsf1o.m ⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
imasdsf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
imasdsf1o.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion imasdsf1o ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) = ( 𝑋 𝐸 𝑌 ) )

Proof

Step Hyp Ref Expression
1 imasdsf1o.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasdsf1o.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasdsf1o.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4 imasdsf1o.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 imasdsf1o.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
6 imasdsf1o.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
7 imasdsf1o.m ⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
8 imasdsf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 imasdsf1o.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10 eqid ⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
11 eqid ⊢ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } = { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) }
12 eqid ⊢ ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) = ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝐹 ‘ 𝑌 ) ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 imasdsf1olem ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) = ( 𝑋 𝐸 𝑌 ) )