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 = ( 1o mPoly R )
	ply1mpl1.p	|- P = ( Poly1 ` R )
	ply1mpl1.o	|- .1. = ( 1r ` P )
Assertion	ply1mpl1	|- .1. = ( 1r ` M )

Proof

Step	Hyp	Ref	Expression
1		ply1mpl1.m	|- M = ( 1o mPoly R )
2		ply1mpl1.p	|- P = ( Poly1 ` R )
3		ply1mpl1.o	|- .1. = ( 1r ` P )
4		eqidd	|- ( T. -> ( Base ` P ) = ( Base ` P ) )
5		eqid	|- ( Base ` P ) = ( Base ` P )
6	2 5	ply1bas	|- ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
7	1	fveq2i	|- ( Base ` M ) = ( Base ` ( 1o mPoly R ) )
8	6 7	eqtr4i	|- ( Base ` P ) = ( Base ` M )
9	8	a1i	|- ( T. -> ( Base ` P ) = ( Base ` M ) )
10		eqid	|- ( .r ` P ) = ( .r ` P )
11	2 1 10	ply1mulr	|- ( .r ` P ) = ( .r ` M )
12	11	a1i	|- ( T. -> ( .r ` P ) = ( .r ` M ) )
13	12	oveqdr	|- ( ( T. /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( .r ` P ) y ) = ( x ( .r ` M ) y ) )
14	4 9 13	rngidpropd	|- ( T. -> ( 1r ` P ) = ( 1r ` M ) )
15	14	mptru	|- ( 1r ` P ) = ( 1r ` M )
16	3 15	eqtri	|- .1. = ( 1r ` M )