Description: The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | psrplusg.s | |- S = ( I mPwSer R ) |
|
| psrplusg.b | |- B = ( Base ` S ) |
||
| psrplusg.a | |- .+ = ( +g ` R ) |
||
| psrplusg.p | |- .+b = ( +g ` S ) |
||
| psradd.x | |- ( ph -> X e. B ) |
||
| psradd.y | |- ( ph -> Y e. B ) |
||
| Assertion | psradd | |- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | psrplusg.s | |- S = ( I mPwSer R ) |
|
| 2 | psrplusg.b | |- B = ( Base ` S ) |
|
| 3 | psrplusg.a | |- .+ = ( +g ` R ) |
|
| 4 | psrplusg.p | |- .+b = ( +g ` S ) |
|
| 5 | psradd.x | |- ( ph -> X e. B ) |
|
| 6 | psradd.y | |- ( ph -> Y e. B ) |
|
| 7 | 1 2 3 4 | psrplusg | |- .+b = ( oF .+ |` ( B X. B ) ) |
| 8 | 7 | oveqi | |- ( X .+b Y ) = ( X ( oF .+ |` ( B X. B ) ) Y ) |
| 9 | 5 6 | ofmresval | |- ( ph -> ( X ( oF .+ |` ( B X. B ) ) Y ) = ( X oF .+ Y ) ) |
| 10 | 8 9 | syl5eq | |- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) ) |