Metamath Proof Explorer


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 sselid ( 𝜑𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
17 15 6 sselid ( 𝜑𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
18 7 8 3 14 16 17 psradd ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑋f + 𝑌 ) )