Theorem psr1crng

Description: The ring of univariate power series is a commutative ring. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypothesis	psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
Assertion	psr1crng	$$⊢R\in \mathrm{CRing}\to S\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
2	1	psr1val	$$⊢S=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
3		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
4	3	a1i	$$⊢R\in \mathrm{CRing}\to 1_{𝑜}\in \mathrm{On}$$
5		id	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{CRing}$$
6		0ss	$$⊢\varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
7	6	a1i	$$⊢R\in \mathrm{CRing}\to \varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
8	2 4 5 7	opsrcrng	$$⊢R\in \mathrm{CRing}\to S\in \mathrm{CRing}$$