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	eqtrid	|- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )