ply1plusgpropd

Description: Property deduction for univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	ply1baspropd.b1	$⊢ φ \to B = {Base}_{R}$
	ply1baspropd.b2	$⊢ φ \to B = {Base}_{S}$
	ply1baspropd.p	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{R} y = x +_{S} y$
Assertion	ply1plusgpropd	$⊢ φ \to +_{{Poly}_{1} (R)} = +_{{Poly}_{1} (S)}$

Step	Hyp	Ref	Expression
1		ply1baspropd.b1	$⊢ φ \to B = {Base}_{R}$
2		ply1baspropd.b2	$⊢ φ \to B = {Base}_{S}$
3		ply1baspropd.p	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{R} y = x +_{S} y$
4	1 2 3	psrplusgpropd	$⊢ φ \to +_{(1_{𝑜} mPwSer R)} = +_{(1_{𝑜} mPwSer S)}$
5		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
6		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
7		eqid	$⊢ +_{(1_{𝑜} mPoly R)} = +_{(1_{𝑜} mPoly R)}$
8	5 6 7	mplplusg	$⊢ +_{(1_{𝑜} mPoly R)} = +_{(1_{𝑜} mPwSer R)}$
9		eqid	$⊢ 1_{𝑜} mPoly S = 1_{𝑜} mPoly S$
10		eqid	$⊢ 1_{𝑜} mPwSer S = 1_{𝑜} mPwSer S$
11		eqid	$⊢ +_{(1_{𝑜} mPoly S)} = +_{(1_{𝑜} mPoly S)}$
12	9 10 11	mplplusg	$⊢ +_{(1_{𝑜} mPoly S)} = +_{(1_{𝑜} mPwSer S)}$
13	4 8 12	3eqtr4g	$⊢ φ \to +_{(1_{𝑜} mPoly R)} = +_{(1_{𝑜} mPoly S)}$
14		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
15		eqid	$⊢ +_{{Poly}_{1} (R)} = +_{{Poly}_{1} (R)}$
16	14 5 15	ply1plusg	$⊢ +_{{Poly}_{1} (R)} = +_{(1_{𝑜} mPoly R)}$
17		eqid	$⊢ {Poly}_{1} (S) = {Poly}_{1} (S)$
18		eqid	$⊢ +_{{Poly}_{1} (S)} = +_{{Poly}_{1} (S)}$
19	17 9 18	ply1plusg	$⊢ +_{{Poly}_{1} (S)} = +_{(1_{𝑜} mPoly S)}$
20	13 16 19	3eqtr4g	$⊢ φ \to +_{{Poly}_{1} (R)} = +_{{Poly}_{1} (S)}$

Metamath Proof Explorer