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 ) |
| 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 ) |