imasds

Description: The distance function of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 11-Jul-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (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)$
Assertion	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)) ℝ^{} <))$

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		eqid	$⊢ +_{R} = +_{R}$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9		eqid	$⊢ Scalar (R) = Scalar (R)$
10		eqid	$⊢ {Base}_{Scalar (R)} = {Base}_{Scalar (R)}$
11		eqid	$⊢ \cdot_{R} = \cdot_{R}$
12		eqid	$⊢ \cdot_{𝑖} (R) = \cdot_{𝑖} (R)$
13		eqid	$⊢ TopOpen (R) = TopOpen (R)$
14		eqid	$⊢ \leq_{R} = \leq_{R}$
15		eqidd	$⊢ φ \to ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\}$
16		eqidd	$⊢ φ \to ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\}$
17		eqidd	$⊢ φ \to ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q)) = ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q))$
18		eqidd	$⊢ φ \to ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}$
19		eqidd	$⊢ φ \to TopOpen (R) qTop F = TopOpen (R) qTop F$
20		eqidd	$⊢ φ \to (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)) ℝ^{} <)) = (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)) ℝ^{} <))$
21		eqidd	$⊢ φ \to (F \circ \leq_{R}) \circ F^{-1} = (F \circ \leq_{R}) \circ F^{-1}$
22	1 2 7 8 9 10 11 12 13 5 14 15 16 17 18 19 20 21 3 4	imasval	$⊢ φ \to U = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (R) qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), (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)) ℝ^{} <))⟩\}$
23		eqid	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (R) qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), (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)) ℝ^{} <))⟩\} = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (R) qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), (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)) ℝ^{} <))⟩\}$
24	23	imasvalstr	$⊢ ((\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (R) qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), (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)) ℝ^{} <))⟩\}) Struct ⟨1, 12⟩$
25		dsid	$⊢ dist = Slot dist (ndx)$
26		snsstp3	$⊢ \{⟨dist (ndx), (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)) ℝ^{} <))⟩\} \subseteq \{⟨TopSet (ndx), TopOpen (R) qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), (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)) ℝ^{} <))⟩\}$
27		ssun2	$⊢ \{⟨TopSet (ndx), TopOpen (R) qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), (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)) ℝ^{} <))⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (R) qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), (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)) ℝ^{} <))⟩\}$
28	26 27	sstri	$⊢ \{⟨dist (ndx), (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)) ℝ^{} <))⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (R) qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), (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)) ℝ^{} <))⟩\}$
29		fvex	$⊢ {Base}_{R} \in V$
30	2 29	eqeltrdi	$⊢ φ \to V \in V$
31		focdmex	$⊢ V \in V \to (F : V \underset{onto}{⟶} B \to B \in V)$
32	30 3 31	sylc	$⊢ φ \to B \in V$
33		mpoexga	$⊢ (B \in V \land B \in V) \to (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)) ℝ^{} <)) \in V$
34	32 32 33	syl2anc	$⊢ φ \to (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)) ℝ^{} <)) \in V$
35	22 24 25 28 34 6	strfv3	$⊢ φ \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)) ℝ^{} <))$

Metamath Proof Explorer

Theorem imasds

Proof