ply1baspropd

Description: Property deduction for univariate polynomial base set. (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	ply1baspropd	$⊢ φ \to {Base}_{{Poly}_{1} (R)} = {Base}_{{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	mplbaspropd	$⊢ φ \to {Base}_{(1_{𝑜} mPoly R)} = {Base}_{(1_{𝑜} mPoly S)}$
5		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
6		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
7	5 6	ply1bas	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{(1_{𝑜} mPoly R)}$
8		eqid	$⊢ {Poly}_{1} (S) = {Poly}_{1} (S)$
9		eqid	$⊢ {Base}_{{Poly}_{1} (S)} = {Base}_{{Poly}_{1} (S)}$
10	8 9	ply1bas	$⊢ {Base}_{{Poly}_{1} (S)} = {Base}_{(1_{𝑜} mPoly S)}$
11	4 7 10	3eqtr4g	$⊢ φ \to {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (S)}$

Metamath Proof Explorer