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