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 𝑃 = ( Poly1𝑅 )
Assertion ply1chr ( 𝑅 ∈ CRing → ( chr ‘ 𝑃 ) = ( chr ‘ 𝑅 ) )

Proof

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