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	$⊢ φ \to U = F “_{𝑠} R$
	imasbas.v	$⊢ φ \to V = {Base}_{R}$
	imasbas.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasbas.r	$⊢ φ \to R \in Z$
	imasds.e	$⊢ E = dist (R)$
	imasds.d	$⊢ D = dist (U)$
	imasdsval.x	$⊢ φ \to X \in B$
	imasdsval.y	$⊢ φ \to Y \in B$
	imasdsval.s	$⊢ S = \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = X \land F (2^{nd} (h (n))) = Y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\}$
	imasds.u	$⊢ T = {E ↾}_{(V \times V)}$
Assertion	imasdsval2	$⊢ φ \to X D Y = inf (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (T \circ g)) ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		imasbas.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasbas.v	$⊢ φ \to V = {Base}_{R}$
3		imasbas.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
4		imasbas.r	$⊢ φ \to R \in Z$
5		imasds.e	$⊢ E = dist (R)$
6		imasds.d	$⊢ D = dist (U)$
7		imasdsval.x	$⊢ φ \to X \in B$
8		imasdsval.y	$⊢ φ \to Y \in B$
9		imasdsval.s	$⊢ S = \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = X \land F (2^{nd} (h (n))) = Y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\}$
10		imasds.u	$⊢ T = {E ↾}_{(V \times V)}$
11	1 2 3 4 5 6 7 8 9	imasdsval	$⊢ φ \to X D Y = inf (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <)$
12	10	coeq1i	$⊢ T \circ g = ({E ↾}_{(V \times V)}) \circ g$
13	9	ssrab3	$⊢ S \subseteq {(V \times V)}^{(1 \dots n)}$
14	13	sseli	$⊢ g \in S \to g \in ({(V \times V)}^{(1 \dots n)})$
15		elmapi	$⊢ g \in ({(V \times V)}^{(1 \dots n)}) \to g : (1 \dots n) ⟶ V \times V$
16		frn	$⊢ g : (1 \dots n) ⟶ V \times V \to ran g \subseteq V \times V$
17		cores	$⊢ ran g \subseteq V \times V \to ({E ↾}_{(V \times V)}) \circ g = E \circ g$
18	14 15 16 17	4syl	$⊢ g \in S \to ({E ↾}_{(V \times V)}) \circ g = E \circ g$
19	12 18	eqtrid	$⊢ g \in S \to T \circ g = E \circ g$
20	19	oveq2d	$⊢ g \in S \to \sum_{ℝ_{𝑠}^{}} (T \circ g) = \sum_{ℝ_{𝑠}^{}} (E \circ g)$
21	20	mpteq2ia	$⊢ (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (T \circ g)) = (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
22	21	rneqi	$⊢ ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (T \circ g)) = ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
23	22	a1i	$⊢ n \in ℕ \to ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (T \circ g)) = ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
24	23	iuneq2i	$⊢ ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (T \circ g)) = ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
25	24	infeq1i	$⊢ inf (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (T \circ g)) ℝ^{} <) = inf (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <)$
26	11 25	eqtr4di	$⊢ φ \to X D Y = inf (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (T \circ g)) ℝ^{} <)$

Metamath Proof Explorer

Theorem imasdsval2

Proof