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	⊢ 𝑀 = ( 1o mPoly 𝑅 )
	ply1mpl1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1mpl1.o	⊢ 1 = ( 1r ‘ 𝑃 )
Assertion	ply1mpl1	⊢ 1 = ( 1r ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		ply1mpl1.m	⊢ 𝑀 = ( 1o mPoly 𝑅 )
2		ply1mpl1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		ply1mpl1.o	⊢ 1 = ( 1r ‘ 𝑃 )
4		eqidd	⊢ ( ⊤ → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) )
5		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
6	2 5	ply1bas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
7	1	fveq2i	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
8	6 7	eqtr4i	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑀 )
9	8	a1i	⊢ ( ⊤ → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑀 ) )
10		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
11	2 1 10	ply1mulr	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑀 )
12	11	a1i	⊢ ( ⊤ → ( .r ‘ 𝑃 ) = ( .r ‘ 𝑀 ) )
13	12	oveqdr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑀 ) 𝑦 ) )
14	4 9 13	rngidpropd	⊢ ( ⊤ → ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑀 ) )
15	14	mptru	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑀 )
16	3 15	eqtri	⊢ 1 = ( 1r ‘ 𝑀 )