Theorem mpladd

Description: The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	mpladd.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mpladd.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mpladd.a	⊢ + = ( +g ‘ 𝑅 )
	mpladd.g	⊢ ✚ = ( +g ‘ 𝑃 )
	mpladd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	mpladd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	mpladd	⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		mpladd.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mpladd.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		mpladd.a	⊢ + = ( +g ‘ 𝑅 )
4		mpladd.g	⊢ ✚ = ( +g ‘ 𝑃 )
5		mpladd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		mpladd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
8		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
9	2	fvexi	⊢ 𝐵 ∈ V
10	1 7 2	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s 𝐵 )
11		eqid	⊢ ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝑅 ) )
12	10 11	ressplusg	⊢ ( 𝐵 ∈ V → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑃 ) )
13	9 12	ax-mp	⊢ ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑃 )
14	4 13	eqtr4i	⊢ ✚ = ( +g ‘ ( 𝐼 mPwSer 𝑅 ) )
15	1 7 2 8	mplbasss	⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
16	15 5	sseldi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
17	15 6	sseldi	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
18	7 8 3 14 16 17	psradd	⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )