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

Metamath Proof Explorer

Theorem mpladd

Description: The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mpladd.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mpladd.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mpladd.a ⊢ + = ( +g ‘ 𝑅 )
mpladd.g ⊢ ✚ = ( +g ‘ 𝑃 )
mpladd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mpladd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion mpladd ( 𝜑 → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mpladd.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mpladd.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 mpladd.a ⊢ + = ( +g ‘ 𝑅 )
4 mpladd.g ⊢ ✚ = ( +g ‘ 𝑃 )
5 mpladd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 mpladd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
8 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
9 1 7 4 mplplusg ⊢ ✚ = ( +g ‘ ( 𝐼 mPwSer 𝑅 ) )
10 1 7 2 8 mplbasss ⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
11 10 5 sselid ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
12 10 6 sselid ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
13 7 8 3 9 11 12 psradd ⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )