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	$⊢ φ \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))))\}$
Assertion	imasdsval	$⊢ φ \to X D Y = sup (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \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	1 2 3 4 5 6	imasds	$⊢ φ \to D = (x \in B, y \in B ⟼ sup (⋃_{n \in ℕ} ran (g \in \{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))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <))$
11		simplrl	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to x = X$
12	11	eqeq2d	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to (F (1^{st} (h (1))) = x \leftrightarrow F (1^{st} (h (1))) = X)$
13		simplrr	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to y = Y$
14	13	eqeq2d	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to (F (2^{nd} (h (n))) = y \leftrightarrow F (2^{nd} (h (n))) = Y)$
15	12 14	3anbi12d	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to ((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)))) \leftrightarrow (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)))))$
16	15	rabbidv	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to \{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))))\} = \{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))))\}$
17	16 9	eqtr4di	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to \{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))))\} = S$
18	17	mpteq1d	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to (g \in \{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))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) = (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
19	18	rneqd	$⊢ ((φ \land (x = X \land y = Y)) \land n \in ℕ) \to ran (g \in \{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))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) = ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
20	19	iuneq2dv	$⊢ (φ \land (x = X \land y = Y)) \to ⋃_{n \in ℕ} ran (g \in \{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))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) = ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
21	20	infeq1d	$⊢ (φ \land (x = X \land y = Y)) \to sup (⋃_{n \in ℕ} ran (g \in \{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))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <) = sup (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <)$
22		xrltso	$⊢ < Or ℝ^{*}$
23	22	infex	$⊢ sup (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <) \in V$
24	23	a1i	$⊢ φ \to sup (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <) \in V$
25	10 21 7 8 24	ovmpod	$⊢ φ \to X D Y = sup (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <)$

Metamath Proof Explorer

Theorem imasdsval

Proof