Theorem imasdsval2

Description: The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by AV, 6-Oct-2020)

	Ref	Expression
Hypotheses	imasbas.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
	imasbas.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imasbas.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
	imasbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
	imasds.e	⊢ 𝐸 = ( dist ‘ 𝑅 )
	imasds.d	⊢ 𝐷 = ( dist ‘ 𝑈 )
	imasdsval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	imasdsval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	imasdsval.s	⊢ 𝑆 = { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑋 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) }
	imasds.u	⊢ 𝑇 = ( 𝐸 ↾ ( 𝑉 × 𝑉 ) )
Assertion	imasdsval2	⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) = inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝑇 ∘ 𝑔 ) ) ) , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		imasbas.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2		imasbas.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imasbas.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4		imasbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5		imasds.e	⊢ 𝐸 = ( dist ‘ 𝑅 )
6		imasds.d	⊢ 𝐷 = ( dist ‘ 𝑈 )
7		imasdsval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		imasdsval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		imasdsval.s	⊢ 𝑆 = { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑋 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) }
10		imasds.u	⊢ 𝑇 = ( 𝐸 ↾ ( 𝑉 × 𝑉 ) )
11	1 2 3 4 5 6 7 8 9	imasdsval	⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) = inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < ) )
12	10	coeq1i	⊢ ( 𝑇 ∘ 𝑔 ) = ( ( 𝐸 ↾ ( 𝑉 × 𝑉 ) ) ∘ 𝑔 )
13	9	ssrab3	⊢ 𝑆 ⊆ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) )
14	13	sseli	⊢ ( 𝑔 ∈ 𝑆 → 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) )
15		elmapi	⊢ ( 𝑔 ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) → 𝑔 : ( 1 ... 𝑛 ) ⟶ ( 𝑉 × 𝑉 ) )
16		frn	⊢ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ( 𝑉 × 𝑉 ) → ran 𝑔 ⊆ ( 𝑉 × 𝑉 ) )
17		cores	⊢ ( ran 𝑔 ⊆ ( 𝑉 × 𝑉 ) → ( ( 𝐸 ↾ ( 𝑉 × 𝑉 ) ) ∘ 𝑔 ) = ( 𝐸 ∘ 𝑔 ) )
18	14 15 16 17	4syl	⊢ ( 𝑔 ∈ 𝑆 → ( ( 𝐸 ↾ ( 𝑉 × 𝑉 ) ) ∘ 𝑔 ) = ( 𝐸 ∘ 𝑔 ) )
19	12 18	syl5eq	⊢ ( 𝑔 ∈ 𝑆 → ( 𝑇 ∘ 𝑔 ) = ( 𝐸 ∘ 𝑔 ) )
20	19	oveq2d	⊢ ( 𝑔 ∈ 𝑆 → ( ℝ*𝑠 Σg ( 𝑇 ∘ 𝑔 ) ) = ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
21	20	mpteq2ia	⊢ ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝑇 ∘ 𝑔 ) ) ) = ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
22	21	rneqi	⊢ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝑇 ∘ 𝑔 ) ) ) = ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
23	22	a1i	⊢ ( 𝑛 ∈ ℕ → ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝑇 ∘ 𝑔 ) ) ) = ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
24	23	iuneq2i	⊢ ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝑇 ∘ 𝑔 ) ) ) = ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) )
25	24	infeq1i	⊢ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝑇 ∘ 𝑔 ) ) ) , ℝ* , < ) = inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < )
26	11 25	eqtr4di	⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) = inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝑇 ∘ 𝑔 ) ) ) , ℝ* , < ) )