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_{𝑜}\mathrm{mPoly}R$$
	ply1mpl0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1mpl0.z	$$⊢\underset{\dot{}}{0}=0_P$$
Assertion	ply1mpl0	$$⊢\underset{\dot{}}{0}=0_M$$

Proof

Step	Hyp	Ref	Expression
1		ply1mpl0.m	$$⊢M=1_{𝑜}\mathrm{mPoly}R$$
2		ply1mpl0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		ply1mpl0.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		eqidd	$$⊢\top \to {\mathrm{Base}}_P={\mathrm{Base}}_P$$
5		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
6	2 5	ply1bas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
7	1	fveq2i	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8	6 7	eqtr4i	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_M$$
9	8	a1i	$$⊢\top \to {\mathrm{Base}}_P={\mathrm{Base}}_M$$
10		eqid	$$⊢{+}_P={+}_P$$
11	2 1 10	ply1plusg	$$⊢{+}_P={+}_M$$
12	11	a1i	$$⊢\top \to {+}_P={+}_M$$
13	12	oveqdr	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_P\wedge y\in {\mathrm{Base}}_P\right)\right)\to x{+}_{P}y=x{+}_{M}y$$
14	4 9 13	grpidpropd	$$⊢\top \to 0_P=0_M$$
15	14	mptru	$$⊢0_P=0_M$$
16	3 15	eqtri	$$⊢\underset{\dot{}}{0}=0_M$$