ply1sca

Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015)

		Ref	Expression
	Hypothesis	ply1lmod.p	$⊢ P = {Poly}_{1} (R)$
	Assertion	ply1sca	$⊢ R \in V \to R = Scalar (P)$

Step	Hyp	Ref	Expression
1		ply1lmod.p	$⊢ P = {Poly}_{1} (R)$
2		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
3	2	psr1sca	$⊢ R \in V \to R = Scalar ({PwSer}_{1} (R))$
4		fvex	$⊢ {Base}_{(1_{𝑜} mPoly R)} \in V$
5	1 2	ply1val	$⊢ P = {PwSer}_{1} (R) ↾_{𝑠} {Base}_{(1_{𝑜} mPoly R)}$
6		eqid	$⊢ Scalar ({PwSer}_{1} (R)) = Scalar ({PwSer}_{1} (R))$
7	5 6	resssca	$⊢ {Base}_{(1_{𝑜} mPoly R)} \in V \to Scalar ({PwSer}_{1} (R)) = Scalar (P)$
8	4 7	ax-mp	$⊢ Scalar ({PwSer}_{1} (R)) = Scalar (P)$
9	3 8	eqtrdi	$⊢ R \in V \to R = Scalar (P)$

Metamath Proof Explorer