Theorem psr1val

Description: Value of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypothesis	psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
Assertion	psr1val	$$⊢S=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
2		oveq2	$$⊢r=R\to 1_{𝑜}\mathrm{ordPwSer}r=1_{𝑜}\mathrm{ordPwSer}R$$
3	2	fveq1d	$$⊢r=R\to \left(1_{𝑜}\mathrm{ordPwSer}r\right)\left(\varnothing \right)=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
4		df-psr1	$$⊢{\mathrm{PwSer}}_1=\left(r\in \mathrm{V}⟼\left(1_{𝑜}\mathrm{ordPwSer}r\right)\left(\varnothing \right)\right)$$
5		fvex	$$⊢\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢R\in \mathrm{V}\to {\mathrm{PwSer}}_1\left(R\right)=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
7		0fv	$$⊢\varnothing \left(\varnothing \right)=\varnothing$$
8	7	eqcomi	$$⊢\varnothing =\varnothing \left(\varnothing \right)$$
9		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{PwSer}}_1\left(R\right)=\varnothing$$
10		reldmopsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{ordPwSer}$$
11	10	ovprc2	$$⊢\neg R\in \mathrm{V}\to 1_{𝑜}\mathrm{ordPwSer}R=\varnothing$$
12	11	fveq1d	$$⊢\neg R\in \mathrm{V}\to \left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)=\varnothing \left(\varnothing \right)$$
13	8 9 12	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to {\mathrm{PwSer}}_1\left(R\right)=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
14	6 13	pm2.61i	$$⊢{\mathrm{PwSer}}_1\left(R\right)=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
15	1 14	eqtri	$$⊢S=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$