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	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐷 ( 𝐹 ‘ 𝑌 ) ) = ( 𝑋 𝐸 𝑌 ) )