Metamath Proof Explorer


Theorem psradd

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

Proof

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