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\mathrm{mPoly}R$$
	mpladd.b	$$⊢B={\mathrm{Base}}_P$$
	mpladd.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	mpladd.g	$$⊢\underset{\dot{}}{✚}={+}_P$$
	mpladd.x	$$⊢\phi \to X\in B$$
	mpladd.y	$$⊢\phi \to Y\in B$$
Assertion	mpladd	$$⊢\phi \to X\underset{\dot{}}{✚}Y=X{\underset{\dot{}}{+}}_{f}Y$$

Proof

Step	Hyp	Ref	Expression
1		mpladd.p	$$⊢P=I\mathrm{mPoly}R$$
2		mpladd.b	$$⊢B={\mathrm{Base}}_P$$
3		mpladd.a	$$⊢\underset{\dot{}}{+}={+}_R$$
4		mpladd.g	$$⊢\underset{\dot{}}{✚}={+}_P$$
5		mpladd.x	$$⊢\phi \to X\in B$$
6		mpladd.y	$$⊢\phi \to Y\in B$$
7		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
9	2	fvexi	$$⊢B\in \mathrm{V}$$
10	1 7 2	mplval2	$$⊢P=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}B$$
11		eqid	$$⊢{+}_{\left(I\mathrm{mPwSer}R\right)}={+}_{\left(I\mathrm{mPwSer}R\right)}$$
12	10 11	ressplusg	$$⊢B\in \mathrm{V}\to {+}_{\left(I\mathrm{mPwSer}R\right)}={+}_P$$
13	9 12	ax-mp	$$⊢{+}_{\left(I\mathrm{mPwSer}R\right)}={+}_P$$
14	4 13	eqtr4i	$$⊢\underset{\dot{}}{✚}={+}_{\left(I\mathrm{mPwSer}R\right)}$$
15	1 7 2 8	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
16	15 5	sseldi	$$⊢\phi \to X\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
17	15 6	sseldi	$$⊢\phi \to Y\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
18	7 8 3 14 16 17	psradd	$$⊢\phi \to X\underset{\dot{}}{✚}Y=X{\underset{\dot{}}{+}}_{f}Y$$