Metamath Proof Explorer

Theorem imasdsval

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 ) ) ) ) ) }
Assertion imasdsval ( 𝜑 → ( 𝑋 𝐷 𝑌 ) = 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 1 2 3 4 5 6 imasds ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < ) ) )
11 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 = 𝑋 )
12 11 eqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ↔ ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑋 ) )
13 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑦 = 𝑌 )
14 13 eqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ↔ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑌 ) )
15 12 14 3anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) ↔ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑋 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
16 15 rabbidv ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } = { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑋 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } )
17 16 9 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } = 𝑆 )
18 17 mpteq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) = ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
19 18 rneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑛 ∈ ℕ ) → ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) = ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
20 19 iuneq2dv ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) = ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) )
21 20 infeq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < ) = inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < ) )
22 xrltso ⊢ < Or ℝ*
23 22 infex ⊢ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < ) ∈ V
24 23 a1i ⊢ ( 𝜑 → inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < ) ∈ V )
25 10 21 7 8 24 ovmpod ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) = inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ 𝑆 ↦ ( ℝ*𝑠 Σg ( 𝐸 ∘ 𝑔 ) ) ) , ℝ* , < ) )