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 = Poly 1 R
Assertion ply1chr R CRing chr P = chr R

Proof

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