Theorem ply1mpl1

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

	Ref	Expression
Hypotheses	ply1mpl1.m	$$⊢M=1_{𝑜}\mathrm{mPoly}R$$
	ply1mpl1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1mpl1.o	$$⊢\underset{\dot{}}{1}=1_P$$
Assertion	ply1mpl1	$$⊢\underset{\dot{}}{1}=1_M$$

Proof

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