Metamath Proof Explorer


Theorem psr1ring

Description: Univariate power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypothesis psr1ring.s 𝑆 = ( PwSer1𝑅 )
Assertion psr1ring ( 𝑅 ∈ Ring → 𝑆 ∈ Ring )

Proof

Step Hyp Ref Expression
1 psr1ring.s 𝑆 = ( PwSer1𝑅 )
2 1 psr1val 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
3 1on 1o ∈ On
4 3 a1i ( 𝑅 ∈ Ring → 1o ∈ On )
5 id ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
6 0ss ∅ ⊆ ( 1o × 1o )
7 6 a1i ( 𝑅 ∈ Ring → ∅ ⊆ ( 1o × 1o ) )
8 2 4 5 7 opsrring ( 𝑅 ∈ Ring → 𝑆 ∈ Ring )