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	sseldi	|- ( ph -> X e. ( Base ` ( I mPwSer R ) ) )
17	15 6	sseldi	|- ( ph -> Y e. ( Base ` ( I mPwSer R ) ) )
18	7 8 3 14 16 17	psradd	|- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )