This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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_{𝑜} mPoly R$
		ply1mpl1.p	$⊢ P = {Poly}_{1} (R)$
		ply1mpl1.o	$⊢ \underset{˙}{1} = 1_{P}$
	Assertion	ply1mpl1	$⊢ \underset{˙}{1} = 1_{M}$

Proof

Step	Hyp	Ref	Expression
1		ply1mpl1.m	$⊢ M = 1_{𝑜} mPoly R$
2		ply1mpl1.p	$⊢ P = {Poly}_{1} (R)$
3		ply1mpl1.o	$⊢ \underset{˙}{1} = 1_{P}$
4		eqidd	$⊢ ⊤ \to {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	$⊢ ⊤ \to {Base}_{P} = {Base}_{M}$
10		eqid	$⊢ \cdot_{P} = \cdot_{P}$
11	2 1 10	ply1mulr	$⊢ \cdot_{P} = \cdot_{M}$
12	11	a1i	$⊢ ⊤ \to \cdot_{P} = \cdot_{M}$
13	12	oveqdr	$⊢ (⊤ \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to x \cdot_{P} y = x \cdot_{M} y$
14	4 9 13	rngidpropd	$⊢ ⊤ \to 1_{P} = 1_{M}$
15	14	mptru	$⊢ 1_{P} = 1_{M}$
16	3 15	eqtri	$⊢ \underset{˙}{1} = 1_{M}$