This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V , r ∈ V ⟼ ⦋ ⨉ x ∈ dom ⁡ r Base r ⁡ x / v⦌ ⦋ f ∈ v , g ∈ v ⟼ ⨉ x ∈ dom ⁡ r f ⁡ x Hom ⁡ r ⁡ x g ⁡ x / h⦌ Base ndx v + ndx f ∈ v , g ∈ v ⟼ x ∈ dom ⁡ r ⟼ f ⁡ x + r ⁡ x g ⁡ x ⋅ ndx f ∈ v , g ∈ v ⟼ x ∈ dom ⁡ r ⟼ f ⁡ x ⋅ r ⁡ x g ⁡ x ∪ Scalar ⁡ ndx s ⋅ ndx f ∈ Base s , g ∈ v ⟼ x ∈ dom ⁡ r ⟼ f ⋅ r ⁡ x g ⁡ x ⋅ 𝑖 ⁡ ndx f ∈ v , g ∈ v ⟼ ∑ s x ∈ dom ⁡ r f ⁡ x ⋅ 𝑖 ⁡ r ⁡ x g ⁡ x ∪ TopSet ⁡ ndx ∏ 𝑡 ⁡ TopOpen ∘ r ≤ ndx f g | f g ⊆ v ∧ ∀ x ∈ dom ⁡ r f ⁡ x ≤ r ⁡ x g ⁡ x dist ⁡ ndx f ∈ v , g ∈ v ⟼ sup ran ⁡ x ∈ dom ⁡ r ⟼ f ⁡ x dist ⁡ r ⁡ x g ⁡ x ∪ 0 ℝ * < ∪ Hom ⁡ ndx h comp ⁡ ndx a ∈ v × v , c ∈ v ⟼ d ∈ 2 nd ⁡ a h c , e ∈ h ⁡ a ⟼ x ∈ dom ⁡ r ⟼ d ⁡ x 1 st ⁡ a ⁡ x 2 nd ⁡ a ⁡ x comp ⁡ r ⁡ x c ⁡ x e ⁡ x
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ ⨉ 𝑠