Metamath Proof Explorer

Theorem reldmprds

Description: The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015) (Revised by Thierry Arnoux, 15-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

		Ref	Expression
	Assertion	reldmprds	$⊢ Rel dom ⨉_{𝑠}$

Proof

Step	Hyp	Ref	Expression
1		df-prds	$⊢ ⨉_{𝑠} = (s \in V, r \in V ⟼ ⦋ \underset{x \in dom r}{⨉} {Base}_{r (x)} / v ⦌ ⦋ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) / h ⦌ ((\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\})))$
2	1	reldmmpo	$⊢ Rel dom ⨉_{𝑠}$