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)

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 ` R ) = ( Base ` R )
6 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
7 5 6 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
8 eqid 
 |-  ( .s ` P ) = ( .s ` P )
9 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
10 5 1 2 8 3 4 9 ply1scltm 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( 1r ` R ) ( .s ` P ) ( 0 .^ X ) ) )
11 7 10 mpdan 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( 1r ` R ) ( .s ` P ) ( 0 .^ X ) ) )
12 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
13 12 fveq2d 
 |-  ( R e. Ring -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
14 13 oveq1d 
 |-  ( R e. Ring -> ( ( 1r ` R ) ( .s ` P ) ( 0 .^ X ) ) = ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 .^ X ) ) )
15 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
16 0nn0 
 |-  0 e. NN0
17 eqid 
 |-  ( Base ` P ) = ( Base ` P )
18 1 2 3 4 17 ply1moncl 
 |-  ( ( R e. Ring /\ 0 e. NN0 ) -> ( 0 .^ X ) e. ( Base ` P ) )
19 16 18 mpan2 
 |-  ( R e. Ring -> ( 0 .^ X ) e. ( Base ` P ) )
20 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
21 eqid 
 |-  ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
22 17 20 8 21 lmodvs1 
 |-  ( ( P e. LMod /\ ( 0 .^ X ) e. ( Base ` P ) ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 .^ X ) ) = ( 0 .^ X ) )
23 15 19 22 syl2anc 
 |-  ( R e. Ring -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 .^ X ) ) = ( 0 .^ X ) )
24 11 14 23 3eqtrrd 
 |-  ( R e. Ring -> ( 0 .^ X ) = ( ( algSc ` P ) ` ( 1r ` R ) ) )
25 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
26 1 9 6 25 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
27 24 26 eqtrd 
 |-  ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) )