Metamath Proof Explorer

Theorem ply1chr

Description: The characteristic of a polynomial ring is the characteristic of the underlying ring. (Contributed by Thierry Arnoux, 24-Jul-2024)

Ref Expression
Hypothesis ply1chr.1 
|- P = ( Poly1 ` R )
Assertion ply1chr 
|- ( R e. CRing -> ( chr ` P ) = ( chr ` R ) )

Proof

Step Hyp Ref Expression
1 ply1chr.1 
 |-  P = ( Poly1 ` R )
2 eqid 
 |-  ( od ` P ) = ( od ` P )
3 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
4 eqid 
 |-  ( chr ` P ) = ( chr ` P )
5 2 3 4 chrval 
 |-  ( ( od ` P ) ` ( 1r ` P ) ) = ( chr ` P )
6 eqid 
 |-  ( od ` R ) = ( od ` R )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 eqid 
 |-  ( chr ` R ) = ( chr ` R )
9 6 7 8 chrval 
 |-  ( ( od ` R ) ` ( 1r ` R ) ) = ( chr ` R )
10 9 eqcomi 
 |-  ( chr ` R ) = ( ( od ` R ) ` ( 1r ` R ) )
11 id 
 |-  ( R e. CRing -> R e. CRing )
12 11 crnggrpd 
 |-  ( R e. CRing -> R e. Grp )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 14 7 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
16 13 15 syl 
 |-  ( R e. CRing -> ( 1r ` R ) e. ( Base ` R ) )
17 8 chrcl 
 |-  ( R e. Ring -> ( chr ` R ) e. NN0 )
18 13 17 syl 
 |-  ( R e. CRing -> ( chr ` R ) e. NN0 )
19 eqid 
 |-  ( .g ` R ) = ( .g ` R )
20 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
21 14 6 19 20 odeq 
 |-  ( ( R e. Grp /\ ( 1r ` R ) e. ( Base ` R ) /\ ( chr ` R ) e. NN0 ) -> ( ( chr ` R ) = ( ( od ` R ) ` ( 1r ` R ) ) <-> A. n e. NN0 ( ( chr ` R ) || n <-> ( n ( .g ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) ) )
22 12 16 18 21 syl3anc 
 |-  ( R e. CRing -> ( ( chr ` R ) = ( ( od ` R ) ` ( 1r ` R ) ) <-> A. n e. NN0 ( ( chr ` R ) || n <-> ( n ( .g ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) ) )
23 10 22 mpbii 
 |-  ( R e. CRing -> A. n e. NN0 ( ( chr ` R ) || n <-> ( n ( .g ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) )
24 23 r19.21bi 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( ( chr ` R ) || n <-> ( n ( .g ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) )
25 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
26 13 adantr 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> R e. Ring )
27 12 grpmndd 
 |-  ( R e. CRing -> R e. Mnd )
28 27 adantr 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> R e. Mnd )
29 simpr 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> n e. NN0 )
30 16 adantr 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( 1r ` R ) e. ( Base ` R ) )
31 14 19 mulgnn0cl 
 |-  ( ( R e. Mnd /\ n e. NN0 /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( n ( .g ` R ) ( 1r ` R ) ) e. ( Base ` R ) )
32 28 29 30 31 syl3anc 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( n ( .g ` R ) ( 1r ` R ) ) e. ( Base ` R ) )
33 simpl 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> R e. CRing )
34 14 20 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
35 33 13 34 3syl 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( 0g ` R ) e. ( Base ` R ) )
36 1 14 25 26 32 35 ply1scleq 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( ( ( algSc ` P ) ` ( n ( .g ` R ) ( 1r ` R ) ) ) = ( ( algSc ` P ) ` ( 0g ` R ) ) <-> ( n ( .g ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) )
37 1 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
38 37 adantr 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> R = ( Scalar ` P ) )
39 38 fveq2d 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( .g ` R ) = ( .g ` ( Scalar ` P ) ) )
40 39 oveqd 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( n ( .g ` R ) ( 1r ` R ) ) = ( n ( .g ` ( Scalar ` P ) ) ( 1r ` R ) ) )
41 40 fveq2d 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( ( algSc ` P ) ` ( n ( .g ` R ) ( 1r ` R ) ) ) = ( ( algSc ` P ) ` ( n ( .g ` ( Scalar ` P ) ) ( 1r ` R ) ) ) )
42 1 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
43 42 adantr 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> P e. AssAlg )
44 38 fveq2d 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
45 30 44 eleqtrd 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( 1r ` R ) e. ( Base ` ( Scalar ` P ) ) )
46 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
47 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
48 eqid 
 |-  ( .g ` P ) = ( .g ` P )
49 eqid 
 |-  ( .g ` ( Scalar ` P ) ) = ( .g ` ( Scalar ` P ) )
50 25 46 47 48 49 asclmulg 
 |-  ( ( P e. AssAlg /\ n e. NN0 /\ ( 1r ` R ) e. ( Base ` ( Scalar ` P ) ) ) -> ( ( algSc ` P ) ` ( n ( .g ` ( Scalar ` P ) ) ( 1r ` R ) ) ) = ( n ( .g ` P ) ( ( algSc ` P ) ` ( 1r ` R ) ) ) )
51 43 29 45 50 syl3anc 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( ( algSc ` P ) ` ( n ( .g ` ( Scalar ` P ) ) ( 1r ` R ) ) ) = ( n ( .g ` P ) ( ( algSc ` P ) ` ( 1r ` R ) ) ) )
52 41 51 eqtrd 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( ( algSc ` P ) ` ( n ( .g ` R ) ( 1r ` R ) ) ) = ( n ( .g ` P ) ( ( algSc ` P ) ` ( 1r ` R ) ) ) )
53 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
54 1 25 20 53 ply1scl0 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
55 33 13 54 3syl 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
56 52 55 eqeq12d 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( ( ( algSc ` P ) ` ( n ( .g ` R ) ( 1r ` R ) ) ) = ( ( algSc ` P ) ` ( 0g ` R ) ) <-> ( n ( .g ` P ) ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( 0g ` P ) ) )
57 24 36 56 3bitr2d 
 |-  ( ( R e. CRing /\ n e. NN0 ) -> ( ( chr ` R ) || n <-> ( n ( .g ` P ) ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( 0g ` P ) ) )
58 57 ralrimiva 
 |-  ( R e. CRing -> A. n e. NN0 ( ( chr ` R ) || n <-> ( n ( .g ` P ) ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( 0g ` P ) ) )
59 1 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
60 59 crnggrpd 
 |-  ( R e. CRing -> P e. Grp )
61 eqid 
 |-  ( Base ` P ) = ( Base ` P )
62 1 25 14 61 ply1sclcl 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( Base ` P ) )
63 13 16 62 syl2anc 
 |-  ( R e. CRing -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( Base ` P ) )
64 61 2 48 53 odeq 
 |-  ( ( P e. Grp /\ ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( Base ` P ) /\ ( chr ` R ) e. NN0 ) -> ( ( chr ` R ) = ( ( od ` P ) ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) <-> A. n e. NN0 ( ( chr ` R ) || n <-> ( n ( .g ` P ) ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( 0g ` P ) ) ) )
65 60 63 18 64 syl3anc 
 |-  ( R e. CRing -> ( ( chr ` R ) = ( ( od ` P ) ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) <-> A. n e. NN0 ( ( chr ` R ) || n <-> ( n ( .g ` P ) ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( 0g ` P ) ) ) )
66 58 65 mpbird 
 |-  ( R e. CRing -> ( chr ` R ) = ( ( od ` P ) ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) )
67 1 25 7 3 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
68 67 fveq2d 
 |-  ( R e. Ring -> ( ( od ` P ) ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( ( od ` P ) ` ( 1r ` P ) ) )
69 13 68 syl 
 |-  ( R e. CRing -> ( ( od ` P ) ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( ( od ` P ) ` ( 1r ` P ) ) )
70 66 69 eqtr2d 
 |-  ( R e. CRing -> ( ( od ` P ) ` ( 1r ` P ) ) = ( chr ` R ) )
71 5 70 syl5eqr 
 |-  ( R e. CRing -> ( chr ` P ) = ( chr ` R ) )