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	$⊢ \underset{˙}{+} = +_{R}$
		mpladd.g	$⊢ \underset{˙}{✚} = +_{P}$
		mpladd.x	$⊢ φ \to X \in B$
		mpladd.y	$⊢ φ \to Y \in B$
	Assertion	mpladd	$⊢ φ \to X \underset{˙}{✚} Y = X {\underset{˙}{+}}_{f} Y$

Proof

Step	Hyp	Ref	Expression
1		mpladd.p	$⊢ P = I mPoly R$
2		mpladd.b	$⊢ B = {Base}_{P}$
3		mpladd.a	$⊢ \underset{˙}{+} = +_{R}$
4		mpladd.g	$⊢ \underset{˙}{✚} = +_{P}$
5		mpladd.x	$⊢ φ \to X \in B$
6		mpladd.y	$⊢ φ \to Y \in B$
7		eqid	$⊢ I mPwSer R = I mPwSer R$
8		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
9	1 7 4	mplplusg	$⊢ \underset{˙}{✚} = +_{(I mPwSer R)}$
10	1 7 2 8	mplbasss	$⊢ B \subseteq {Base}_{(I mPwSer R)}$
11	10 5	sselid	$⊢ φ \to X \in {Base}_{(I mPwSer R)}$
12	10 6	sselid	$⊢ φ \to Y \in {Base}_{(I mPwSer R)}$
13	7 8 3 9 11 12	psradd	$⊢ φ \to X \underset{˙}{✚} Y = X {\underset{˙}{+}}_{f} Y$