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	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
7	2 5 6	ply1bas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
8	1	fveq2i	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
9	7 8	eqtr4i	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑀 )
10	9	a1i	⊢ ( ⊤ → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑀 ) )
11		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
12	2 1 11	ply1mulr	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑀 )
13	12	a1i	⊢ ( ⊤ → ( .r ‘ 𝑃 ) = ( .r ‘ 𝑀 ) )
14	13	oveqdr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑀 ) 𝑦 ) )
15	4 10 14	rngidpropd	⊢ ( ⊤ → ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑀 ) )
16	15	mptru	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑀 )
17	3 16	eqtri	⊢ 1 = ( 1r ‘ 𝑀 )