Metamath Proof Explorer


Theorem psr1mulr

Description: Value of multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses psr1plusg.y
|- Y = ( PwSer1 ` R )
psr1plusg.s
|- S = ( 1o mPwSer R )
psr1mulr.n
|- .x. = ( .r ` Y )
Assertion psr1mulr
|- .x. = ( .r ` S )

Proof

Step Hyp Ref Expression
1 psr1plusg.y
 |-  Y = ( PwSer1 ` R )
2 psr1plusg.s
 |-  S = ( 1o mPwSer R )
3 psr1mulr.n
 |-  .x. = ( .r ` Y )
4 1 psr1val
 |-  Y = ( ( 1o ordPwSer R ) ` (/) )
5 0ss
 |-  (/) C_ ( 1o X. 1o )
6 5 a1i
 |-  ( T. -> (/) C_ ( 1o X. 1o ) )
7 2 4 6 opsrmulr
 |-  ( T. -> ( .r ` S ) = ( .r ` Y ) )
8 7 mptru
 |-  ( .r ` S ) = ( .r ` Y )
9 3 8 eqtr4i
 |-  .x. = ( .r ` S )