Metamath Proof Explorer

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 ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{PwSer}}_{1}\left({R}\right)=\varnothing$
10 reldmopsr ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{ordPwSer}$
11 10 ovprc2 ${⊢}¬{R}\in \mathrm{V}\to {1}_{𝑜}\mathrm{ordPwSer}{R}=\varnothing$
12 11 fveq1d ${⊢}¬{R}\in \mathrm{V}\to \left({1}_{𝑜}\mathrm{ordPwSer}{R}\right)\left(\varnothing \right)=\varnothing \left(\varnothing \right)$
13 8 9 12 3eqtr4a ${⊢}¬{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)$