This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = PwSer 1 ⁡ R
Assertion psr1val ⊢ S = 1 𝑜 ordPwSer R ⁡ ∅

Proof

Step Hyp Ref Expression
1 psr1val.1 ⊢ S = PwSer 1 ⁡ R
2 oveq2 ⊢ r = R → 1 𝑜 ordPwSer r = 1 𝑜 ordPwSer R
3 2 fveq1d ⊢ r = R → 1 𝑜 ordPwSer r ⁡ ∅ = 1 𝑜 ordPwSer R ⁡ ∅
4 df-psr1 ⊢ PwSer 1 = r ∈ V ⟼ 1 𝑜 ordPwSer r ⁡ ∅
5 fvex ⊢ 1 𝑜 ordPwSer R ⁡ ∅ ∈ V
6 3 4 5 fvmpt ⊢ R ∈ V → PwSer 1 ⁡ R = 1 𝑜 ordPwSer R ⁡ ∅
7 0fv ⊢ ∅ ⁡ ∅ = ∅
8 7 eqcomi ⊢ ∅ = ∅ ⁡ ∅
9 fvprc ⊢ ¬ R ∈ V → PwSer 1 ⁡ R = ∅
10 reldmopsr ⊢ Rel ⁡ dom ⁡ ordPwSer
11 10 ovprc2 ⊢ ¬ R ∈ V → 1 𝑜 ordPwSer R = ∅
12 11 fveq1d ⊢ ¬ R ∈ V → 1 𝑜 ordPwSer R ⁡ ∅ = ∅ ⁡ ∅
13 8 9 12 3eqtr4a ⊢ ¬ R ∈ V → PwSer 1 ⁡ R = 1 𝑜 ordPwSer R ⁡ ∅
14 6 13 pm2.61i ⊢ PwSer 1 ⁡ R = 1 𝑜 ordPwSer R ⁡ ∅
15 1 14 eqtri ⊢ S = 1 𝑜 ordPwSer R ⁡ ∅