This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1bas

Description: The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015) Remove hypothesis. (Revised by SN, 20-May-2025)

		Ref	Expression
	Hypotheses	ply1val.1	$⊢ P = {Poly}_{1} (R)$
		ply1bas.u	$⊢ U = {Base}_{P}$
	Assertion	ply1bas	$⊢ U = {Base}_{(1_{𝑜} mPoly R)}$

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	$⊢ P = {Poly}_{1} (R)$
2		ply1bas.u	$⊢ U = {Base}_{P}$
3		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
4		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
5		eqid	$⊢ {Base}_{(1_{𝑜} mPoly R)} = {Base}_{(1_{𝑜} mPoly R)}$
6		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
7		eqid	$⊢ {Base}_{{PwSer}_{1} (R)} = {Base}_{{PwSer}_{1} (R)}$
8	6 7 4	psr1bas2	$⊢ {Base}_{{PwSer}_{1} (R)} = {Base}_{(1_{𝑜} mPwSer R)}$
9	3 4 5 8	mplbasss	$⊢ {Base}_{(1_{𝑜} mPoly R)} \subseteq {Base}_{{PwSer}_{1} (R)}$
10	1 6	ply1val	$⊢ P = {PwSer}_{1} (R) ↾_{𝑠} {Base}_{(1_{𝑜} mPoly R)}$
11	10 7	ressbas2	$⊢ {Base}_{(1_{𝑜} mPoly R)} \subseteq {Base}_{{PwSer}_{1} (R)} \to {Base}_{(1_{𝑜} mPoly R)} = {Base}_{P}$
12	9 11	ax-mp	$⊢ {Base}_{(1_{𝑜} mPoly R)} = {Base}_{P}$
13	2 12	eqtr4i	$⊢ U = {Base}_{(1_{𝑜} mPoly R)}$