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 ⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
Assertion psr1val 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )

Proof

Step Hyp Ref Expression
1 psr1val.1 ⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
2 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 1o ordPwSer 𝑟 ) = ( 1o ordPwSer 𝑅 ) )
3 2 fveq1d ⊢ ( 𝑟 = 𝑅 → ( ( 1o ordPwSer 𝑟 ) ‘ ∅ ) = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) )
4 df-psr1 ⊢ PwSer1 = ( 𝑟 ∈ V ↦ ( ( 1o ordPwSer 𝑟 ) ‘ ∅ ) )
5 fvex ⊢ ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) ∈ V
6 3 4 5 fvmpt ⊢ ( 𝑅 ∈ V → ( PwSer1 ‘ 𝑅 ) = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) )
7 0fv ⊢ ( ∅ ‘ ∅ ) = ∅
8 7 eqcomi ⊢ ∅ = ( ∅ ‘ ∅ )
9 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( PwSer1 ‘ 𝑅 ) = ∅ )
10 reldmopsr ⊢ Rel dom ordPwSer
11 10 ovprc2 ⊢ ( ¬ 𝑅 ∈ V → ( 1o ordPwSer 𝑅 ) = ∅ )
12 11 fveq1d ⊢ ( ¬ 𝑅 ∈ V → ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) = ( ∅ ‘ ∅ ) )
13 8 9 12 3eqtr4a ⊢ ( ¬ 𝑅 ∈ V → ( PwSer1 ‘ 𝑅 ) = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) )
14 6 13 pm2.61i ⊢ ( PwSer1 ‘ 𝑅 ) = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
15 1 14 eqtri ⊢ 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )