Theorem psr1sca

Description: Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 4-Jul-2015)

	Ref	Expression
Hypothesis	psr1lmod.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
Assertion	psr1sca	$$⊢R\in V\to R=\mathrm{Scalar}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		psr1lmod.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
2		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
3	1	psr1val	$$⊢P=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
4		0ss	$$⊢\varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
5	4	a1i	$$⊢R\in V\to \varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
6		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
7	6	a1i	$$⊢R\in V\to 1_{𝑜}\in \mathrm{On}$$
8		id	$$⊢R\in V\to R\in V$$
9	2 3 5 7 8	opsrsca	$$⊢R\in V\to R=\mathrm{Scalar}\left(P\right)$$