Metamath Proof Explorer


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 eqtrid ( 𝑔𝑆 → ( 𝑇𝑔 ) = ( 𝐸𝑔 ) )
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 ( 𝑇𝑔 ) ) ) , ℝ* , < ) )