Metamath Proof Explorer


Theorem psr1assa

Description: The ring of univariate power series is an associative algebra. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypothesis psr1val.1
|- S = ( PwSer1 ` R )
Assertion psr1assa
|- ( R e. CRing -> S e. AssAlg )

Proof

Step Hyp Ref Expression
1 psr1val.1
 |-  S = ( PwSer1 ` R )
2 1 psr1val
 |-  S = ( ( 1o ordPwSer R ) ` (/) )
3 1on
 |-  1o e. On
4 3 a1i
 |-  ( R e. CRing -> 1o e. On )
5 id
 |-  ( R e. CRing -> R e. CRing )
6 0ss
 |-  (/) C_ ( 1o X. 1o )
7 6 a1i
 |-  ( R e. CRing -> (/) C_ ( 1o X. 1o ) )
8 2 4 5 7 opsrassa
 |-  ( R e. CRing -> S e. AssAlg )