prdsds

Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

	Ref	Expression
Hypotheses	prdsbas.p	$⊢ P = S ⨉_{𝑠} R$
	prdsbas.s	$⊢ φ \to S \in V$
	prdsbas.r	$⊢ φ \to R \in W$
	prdsbas.b	$⊢ B = {Base}_{P}$
	prdsbas.i	$⊢ φ \to dom R = I$
	prdsds.l	$⊢ D = dist (P)$
Assertion	prdsds	$⊢ φ \to D = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))$

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	$⊢ P = S ⨉_{𝑠} R$
2		prdsbas.s	$⊢ φ \to S \in V$
3		prdsbas.r	$⊢ φ \to R \in W$
4		prdsbas.b	$⊢ B = {Base}_{P}$
5		prdsbas.i	$⊢ φ \to dom R = I$
6		prdsds.l	$⊢ D = dist (P)$
7		eqid	$⊢ {Base}_{S} = {Base}_{S}$
8	1 2 3 4 5	prdsbas	$⊢ φ \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
9		eqid	$⊢ +_{P} = +_{P}$
10	1 2 3 4 5 9	prdsplusg	$⊢ φ \to +_{P} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
11		eqid	$⊢ \cdot_{P} = \cdot_{P}$
12	1 2 3 4 5 11	prdsmulr	$⊢ φ \to \cdot_{P} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
13		eqid	$⊢ \cdot_{P} = \cdot_{P}$
14	1 2 3 4 5 7 13	prdsvsca	$⊢ φ \to \cdot_{P} = (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
15		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x))) = (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))$
16		eqidd	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) = \prod_{𝑡} (TopOpen \circ R)$
17		eqid	$⊢ \leq_{P} = \leq_{P}$
18	1 2 3 4 5 17	prdsle	$⊢ φ \to \leq_{P} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
19		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <)) = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))$
20		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$
21		eqidd	$⊢ φ \to (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x)))) = (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
22	1 7 5 8 10 12 14 15 16 18 19 20 21 2 3	prdsval	$⊢ φ \to P = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{P}⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
23		dsid	$⊢ dist = Slot dist (ndx)$
24	4	fvexi	$⊢ B \in V$
25		xrex	$⊢ ℝ^{*} \in V$
26	25	uniex	$⊢ ⋃ ℝ^{*} \in V$
27	26	pwex	$⊢ 𝒫 ⋃ ℝ^{*} \in V$
28		df-sup	$⊢ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <) = ⋃ \{y \in ℝ^{} \| (\forall z \in (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}) \neg y < z \land \forall z \in ℝ^{*} (z < y \to \exists w \in (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}) z < w))\}$
29		ssrab2	$⊢ \{y \in ℝ^{} \| (\forall z \in (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}) \neg y < z \land \forall z \in ℝ^{} (z < y \to \exists w \in (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}) z < w))\} \subseteq ℝ^{*}$
30	29	unissi	$⊢ ⋃ \{y \in ℝ^{} \| (\forall z \in (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}) \neg y < z \land \forall z \in ℝ^{} (z < y \to \exists w \in (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}) z < w))\} \subseteq ⋃ ℝ^{*}$
31	26 30	elpwi2	$⊢ ⋃ \{y \in ℝ^{} \| (\forall z \in (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}) \neg y < z \land \forall z \in ℝ^{} (z < y \to \exists w \in (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}) z < w))\} \in 𝒫 ⋃ ℝ^{*}$
32	28 31	eqeltri	$⊢ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <) \in 𝒫 ⋃ ℝ^{}$
33	32	rgen2w	$⊢ \forall f \in B \forall g \in B sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <) \in 𝒫 ⋃ ℝ^{}$
34	24 24 27 33	mpoexw	$⊢ (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <)) \in V$
35	34	a1i	$⊢ φ \to (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <)) \in V$
36		snsstp3	$⊢ \{⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \subseteq \{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\}$
37		ssun1	$⊢ \{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \subseteq \{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\}$
38	36 37	sstri	$⊢ \{⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \subseteq \{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\}$
39		ssun2	$⊢ \{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{P}⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
40	38 39	sstri	$⊢ \{⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{P}⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
41	22 6 23 35 40	prdsbaslem	$⊢ φ \to D = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))$

Metamath Proof Explorer

Theorem prdsds

Proof