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
|- .+ = ( +g ` R )
mpladd.g
|- .+b = ( +g ` P )
mpladd.x
|- ( ph -> X e. B )
mpladd.y
|- ( ph -> Y e. B )
Assertion mpladd
|- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )

Proof

Step Hyp Ref Expression
1 mpladd.p
 |-  P = ( I mPoly R )
2 mpladd.b
 |-  B = ( Base ` P )
3 mpladd.a
 |-  .+ = ( +g ` R )
4 mpladd.g
 |-  .+b = ( +g ` P )
5 mpladd.x
 |-  ( ph -> X e. B )
6 mpladd.y
 |-  ( ph -> Y e. B )
7 eqid
 |-  ( I mPwSer R ) = ( I mPwSer R )
8 eqid
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
9 2 fvexi
 |-  B e. _V
10 1 7 2 mplval2
 |-  P = ( ( I mPwSer R ) |`s B )
11 eqid
 |-  ( +g ` ( I mPwSer R ) ) = ( +g ` ( I mPwSer R ) )
12 10 11 ressplusg
 |-  ( B e. _V -> ( +g ` ( I mPwSer R ) ) = ( +g ` P ) )
13 9 12 ax-mp
 |-  ( +g ` ( I mPwSer R ) ) = ( +g ` P )
14 4 13 eqtr4i
 |-  .+b = ( +g ` ( I mPwSer R ) )
15 1 7 2 8 mplbasss
 |-  B C_ ( Base ` ( I mPwSer R ) )
16 15 5 sselid
 |-  ( ph -> X e. ( Base ` ( I mPwSer R ) ) )
17 15 6 sselid
 |-  ( ph -> Y e. ( Base ` ( I mPwSer R ) ) )
18 7 8 3 14 16 17 psradd
 |-  ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )