Metamath Proof Explorer


Theorem ply1mpl0

Description: The univariate polynomial ring has the same zero as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses ply1mpl0.m M = 1 𝑜 mPoly R
ply1mpl0.p P = Poly 1 R
ply1mpl0.z 0 ˙ = 0 P
Assertion ply1mpl0 0 ˙ = 0 M

Proof

Step Hyp Ref Expression
1 ply1mpl0.m M = 1 𝑜 mPoly R
2 ply1mpl0.p P = Poly 1 R
3 ply1mpl0.z 0 ˙ = 0 P
4 eqidd Base P = Base P
5 eqid Base P = Base P
6 2 5 ply1bas Base P = Base 1 𝑜 mPoly R
7 1 fveq2i Base M = Base 1 𝑜 mPoly R
8 6 7 eqtr4i Base P = Base M
9 8 a1i Base P = Base M
10 eqid + P = + P
11 2 1 10 ply1plusg + P = + M
12 11 a1i + P = + M
13 12 oveqdr x Base P y Base P x + P y = x + M y
14 4 9 13 grpidpropd 0 P = 0 M
15 14 mptru 0 P = 0 M
16 3 15 eqtri 0 ˙ = 0 M