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
|- P = ( Poly1 ` R )
ply1idvr1.x
|- X = ( var1 ` R )
ply1idvr1.n
|- N = ( mulGrp ` P )
ply1idvr1.e
|- .^ = ( .g ` N )
Assertion ply1idvr1
|- ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) )

Proof

Step Hyp Ref Expression
1 ply1idvr1.p
 |-  P = ( Poly1 ` R )
2 ply1idvr1.x
 |-  X = ( var1 ` R )
3 ply1idvr1.n
 |-  N = ( mulGrp ` P )
4 ply1idvr1.e
 |-  .^ = ( .g ` N )
5 eqid
 |-  ( Base ` P ) = ( Base ` P )
6 2 1 5 vr1cl
 |-  ( R e. Ring -> X e. ( Base ` P ) )
7 3 5 mgpbas
 |-  ( Base ` P ) = ( Base ` N )
8 eqid
 |-  ( 1r ` P ) = ( 1r ` P )
9 3 8 ringidval
 |-  ( 1r ` P ) = ( 0g ` N )
10 7 9 4 mulg0
 |-  ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
11 6 10 syl
 |-  ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) )