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 P = I mPoly R
mpladd.b B = Base P
mpladd.a + ˙ = + R
mpladd.g ˙ = + P
mpladd.x φ X B
mpladd.y φ Y B
Assertion mpladd φ X ˙ Y = X + ˙ f Y

Proof

Step Hyp Ref Expression
1 mpladd.p P = I mPoly R
2 mpladd.b B = Base P
3 mpladd.a + ˙ = + R
4 mpladd.g ˙ = + P
5 mpladd.x φ X B
6 mpladd.y φ Y B
7 eqid I mPwSer R = I mPwSer R
8 eqid Base I mPwSer R = Base I mPwSer R
9 2 fvexi B V
10 1 7 2 mplval2 P = I mPwSer R 𝑠 B
11 eqid + I mPwSer R = + I mPwSer R
12 10 11 ressplusg B V + I mPwSer R = + P
13 9 12 ax-mp + I mPwSer R = + P
14 4 13 eqtr4i ˙ = + I mPwSer R
15 1 7 2 8 mplbasss B Base I mPwSer R
16 15 5 sselid φ X Base I mPwSer R
17 15 6 sselid φ Y Base I mPwSer R
18 7 8 3 14 16 17 psradd φ X ˙ Y = X + ˙ f Y