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 ⊢ 𝑀 = ( 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 ‘ 𝑀 )