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 
|- 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 1 7 4 mplplusg 
 |-  .+b = ( +g ` ( I mPwSer R ) )
10 1 7 2 8 mplbasss 
 |-  B C_ ( Base ` ( I mPwSer R ) )
11 10 5 sselid 
 |-  ( ph -> X e. ( Base ` ( I mPwSer R ) ) )
12 10 6 sselid 
 |-  ( ph -> Y e. ( Base ` ( I mPwSer R ) ) )
13 7 8 3 9 11 12 psradd 
 |-  ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )