Theorem psradd

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

	Ref	Expression
Hypotheses	psrplusg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrplusg.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psrplusg.a	⊢ + = ( +g ‘ 𝑅 )
	psrplusg.p	⊢ ✚ = ( +g ‘ 𝑆 )
	psradd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	psradd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	psradd	⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		psrplusg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrplusg.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		psrplusg.a	⊢ + = ( +g ‘ 𝑅 )
4		psrplusg.p	⊢ ✚ = ( +g ‘ 𝑆 )
5		psradd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		psradd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7	1 2 3 4	psrplusg	⊢ ✚ = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )
8	7	oveqi	⊢ ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) 𝑌 )
9	5 6	ofmresval	⊢ ( 𝜑 → ( 𝑋 ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )
10	8 9	syl5eq	⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )