Metamath Proof Explorer


Theorem ply1idvr1

Description: The identity of a polynomial ring expressed as power of the polynomial variable. (Contributed by AV, 14-Aug-2019) (Proof shortened by SN, 3-Jul-2025)

Ref Expression
Hypotheses ply1idvr1.p 𝑃 = ( Poly1𝑅 )
ply1idvr1.x 𝑋 = ( var1𝑅 )
ply1idvr1.n 𝑁 = ( mulGrp ‘ 𝑃 )
ply1idvr1.e = ( .g𝑁 )
Assertion ply1idvr1 ( 𝑅 ∈ Ring → ( 0 𝑋 ) = ( 1r𝑃 ) )

Proof

Step Hyp Ref Expression
1 ply1idvr1.p 𝑃 = ( Poly1𝑅 )
2 ply1idvr1.x 𝑋 = ( var1𝑅 )
3 ply1idvr1.n 𝑁 = ( mulGrp ‘ 𝑃 )
4 ply1idvr1.e = ( .g𝑁 )
5 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
6 2 1 5 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
7 3 5 mgpbas ( Base ‘ 𝑃 ) = ( Base ‘ 𝑁 )
8 eqid ( 1r𝑃 ) = ( 1r𝑃 )
9 3 8 ringidval ( 1r𝑃 ) = ( 0g𝑁 )
10 7 9 4 mulg0 ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 𝑋 ) = ( 1r𝑃 ) )
11 6 10 syl ( 𝑅 ∈ Ring → ( 0 𝑋 ) = ( 1r𝑃 ) )