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

Metamath Proof Explorer

Theorem reldmpsr

Description: The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion reldmpsr ⊢ Rel ⁡ dom ⁡ mPwSer

Proof

Step Hyp Ref Expression
1 df-psr ⊢ mPwSer = i ∈ V , r ∈ V ⟼ ⦋ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d⦌ ⦋ Base r d / b⦌ Base ndx b + ndx ∘ f ⁡ + r ↾ b × b ⋅ ndx f ∈ b , g ∈ b ⟼ k ∈ d ⟼ ∑ r x ∈ y ∈ d | y ≤ f k f ⁡ x ⋅ r g ⁡ k − f x ∪ Scalar ⁡ ndx r ⋅ ndx x ∈ Base r , f ∈ b ⟼ d × x ⋅ r f f TopSet ⁡ ndx ∏ 𝑡 ⁡ d × TopOpen ⁡ r
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ mPwSer