psradd

Description: The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

Step	Hyp	Ref	Expression
1		psrplusg.s	$⊢ S = I mPwSer R$
2		psrplusg.b	$⊢ B = {Base}_{S}$
3		psrplusg.a	$⊢ \underset{˙}{+} = +_{R}$
4		psrplusg.p	$⊢ \underset{˙}{✚} = +_{S}$
5		psradd.x	$⊢ φ \to X \in B$
6		psradd.y	$⊢ φ \to Y \in B$
7	1 2 3 4	psrplusg	$⊢ \underset{˙}{✚} = {\circ_{f} \underset{˙}{+} ↾}_{(B \times B)}$
8	7	oveqi	$⊢ X \underset{˙}{✚} Y = X ({\circ_{f} \underset{˙}{+} ↾}_{(B \times B)}) Y$
9	5 6	ofmresval	$⊢ φ \to X ({\circ_{f} \underset{˙}{+} ↾}_{(B \times B)}) Y = X {\underset{˙}{+}}_{f} Y$
10	8 9	eqtrid	$⊢ φ \to X \underset{˙}{✚} Y = X {\underset{˙}{+}}_{f} Y$

Metamath Proof Explorer