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\mathrm{mPwSer}R$$
	psrplusg.b	$$⊢B={\mathrm{Base}}_S$$
	psrplusg.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	psrplusg.p	$$⊢\underset{\dot{}}{✚}={+}_S$$
	psradd.x	$$⊢\phi \to X\in B$$
	psradd.y	$$⊢\phi \to Y\in B$$
Assertion	psradd	$$⊢\phi \to X\underset{\dot{}}{✚}Y=X{\underset{\dot{}}{+}}_{f}Y$$

Proof

Step	Hyp	Ref	Expression
1		psrplusg.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrplusg.b	$$⊢B={\mathrm{Base}}_S$$
3		psrplusg.a	$$⊢\underset{\dot{}}{+}={+}_R$$
4		psrplusg.p	$$⊢\underset{\dot{}}{✚}={+}_S$$
5		psradd.x	$$⊢\phi \to X\in B$$
6		psradd.y	$$⊢\phi \to Y\in B$$
7	1 2 3 4	psrplusg	$$⊢\underset{\dot{}}{✚}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$
8	7	oveqi	$$⊢X\underset{\dot{}}{✚}Y=X\left({{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)Y$$
9	5 6	ofmresval	$$⊢\phi \to X\left({{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)Y=X{\underset{\dot{}}{+}}_{f}Y$$
10	8 9	syl5eq	$$⊢\phi \to X\underset{\dot{}}{✚}Y=X{\underset{\dot{}}{+}}_{f}Y$$