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 ⊢ φ → U = F “ 𝑠 R
imasbas.v ⊢ φ → V = Base R
imasbas.f ⊢ φ → F : V ⟶ onto B
imasbas.r ⊢ φ → R ∈ Z
imasds.e ⊢ E = dist ⁡ R
imasds.d ⊢ D = dist ⁡ U
imasdsval.x ⊢ φ → X ∈ B
imasdsval.y ⊢ φ → Y ∈ B
imasdsval.s ⊢ S = h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = X ∧ F ⁡ 2 nd ⁡ h ⁡ n = Y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1
Assertion imasdsval ⊢ φ → X D Y = inf ⋃ n ∈ ℕ ran ⁡ g ∈ S ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * <

Proof

Step Hyp Ref Expression
1 imasbas.u ⊢ φ → U = F “ 𝑠 R
2 imasbas.v ⊢ φ → V = Base R
3 imasbas.f ⊢ φ → F : V ⟶ onto B
4 imasbas.r ⊢ φ → R ∈ Z
5 imasds.e ⊢ E = dist ⁡ R
6 imasds.d ⊢ D = dist ⁡ U
7 imasdsval.x ⊢ φ → X ∈ B
8 imasdsval.y ⊢ φ → Y ∈ B
9 imasdsval.s ⊢ S = h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = X ∧ F ⁡ 2 nd ⁡ h ⁡ n = Y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1
10 1 2 3 4 5 6 imasds ⊢ φ → D = x ∈ B , y ∈ B ⟼ inf ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * <
11 simplrl ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → x = X
12 11 eqeq2d ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → F ⁡ 1 st ⁡ h ⁡ 1 = x ↔ F ⁡ 1 st ⁡ h ⁡ 1 = X
13 simplrr ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → y = Y
14 13 eqeq2d ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → F ⁡ 2 nd ⁡ h ⁡ n = y ↔ F ⁡ 2 nd ⁡ h ⁡ n = Y
15 12 14 3anbi12d ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ↔ F ⁡ 1 st ⁡ h ⁡ 1 = X ∧ F ⁡ 2 nd ⁡ h ⁡ n = Y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1
16 15 rabbidv ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 = h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = X ∧ F ⁡ 2 nd ⁡ h ⁡ n = Y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1
17 16 9 eqtr4di ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 = S
18 17 mpteq1d ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g = g ∈ S ⟼ ∑ ℝ 𝑠 * E ∘ g
19 18 rneqd ⊢ φ ∧ x = X ∧ y = Y ∧ n ∈ ℕ → ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g = ran ⁡ g ∈ S ⟼ ∑ ℝ 𝑠 * E ∘ g
20 19 iuneq2dv ⊢ φ ∧ x = X ∧ y = Y → ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g = ⋃ n ∈ ℕ ran ⁡ g ∈ S ⟼ ∑ ℝ 𝑠 * E ∘ g
21 20 infeq1d ⊢ φ ∧ x = X ∧ y = Y → inf ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * < = inf ⋃ n ∈ ℕ ran ⁡ g ∈ S ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * <
22 xrltso ⊢ < Or ℝ *
23 22 infex ⊢ inf ⋃ n ∈ ℕ ran ⁡ g ∈ S ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * < ∈ V
24 23 a1i ⊢ φ → inf ⋃ n ∈ ℕ ran ⁡ g ∈ S ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * < ∈ V
25 10 21 7 8 24 ovmpod ⊢ φ → X D Y = inf ⋃ n ∈ ℕ ran ⁡ g ∈ S ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * <