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 28 29 30 mulgnn0cld ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
32 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ CRing )
33 14 20 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
34 32 13 33 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
35 1 14 25 26 31 34 ply1scleq ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) ↔ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
36 1 ply1sca ⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
37 36 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
38 37 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( .g ‘ 𝑅 ) = ( .g ‘ ( Scalar ‘ 𝑃 ) ) )
39 38 oveqd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑛 ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( 1r ‘ 𝑅 ) ) )
40 39 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑛 ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( 1r ‘ 𝑅 ) ) ) )
41 1 ply1assa ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
42 41 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → 𝑃 ∈ AssAlg )
43 37 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
44 30 43 eleqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
45 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
46 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
47 eqid ⊢ ( .g ‘ 𝑃 ) = ( .g ‘ 𝑃 )
48 eqid ⊢ ( .g ‘ ( Scalar ‘ 𝑃 ) ) = ( .g ‘ ( Scalar ‘ 𝑃 ) )
49 25 45 46 47 48 asclmulg ⊢ ( ( 𝑃 ∈ AssAlg ∧ 𝑛 ∈ ℕ0 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑛 ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑛 ( .g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
50 42 29 44 49 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑛 ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑛 ( .g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
51 40 50 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑛 ( .g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
52 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
53 1 25 20 52 ply1scl0 ⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
54 32 13 53 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
55 51 54 eqeq12d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑅 ) ) ↔ ( 𝑛 ( .g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ) )
56 24 35 55 3bitr2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0 ) → ( ( chr ‘ 𝑅 ) ∥ 𝑛 ↔ ( 𝑛 ( .g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ) )
57 56 ralrimiva ⊢ ( 𝑅 ∈ CRing → ∀ 𝑛 ∈ ℕ0 ( ( chr ‘ 𝑅 ) ∥ 𝑛 ↔ ( 𝑛 ( .g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ) )
58 1 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
59 58 crnggrpd ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Grp )
60 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
61 1 25 14 60 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
62 13 16 61 syl2anc ⊢ ( 𝑅 ∈ CRing → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
63 60 2 47 52 odeq ⊢ ( ( 𝑃 ∈ Grp ∧ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) ∧ ( chr ‘ 𝑅 ) ∈ ℕ0 ) → ( ( chr ‘ 𝑅 ) = ( ( od ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( chr ‘ 𝑅 ) ∥ 𝑛 ↔ ( 𝑛 ( .g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ) ) )
64 59 62 18 63 syl3anc ⊢ ( 𝑅 ∈ CRing → ( ( chr ‘ 𝑅 ) = ( ( od ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( chr ‘ 𝑅 ) ∥ 𝑛 ↔ ( 𝑛 ( .g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ) ) )
65 57 64 mpbird ⊢ ( 𝑅 ∈ CRing → ( chr ‘ 𝑅 ) = ( ( od ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
66 1 25 7 3 ply1scl1 ⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
67 66 fveq2d ⊢ ( 𝑅 ∈ Ring → ( ( od ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( od ‘ 𝑃 ) ‘ ( 1r ‘ 𝑃 ) ) )
68 13 67 syl ⊢ ( 𝑅 ∈ CRing → ( ( od ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( od ‘ 𝑃 ) ‘ ( 1r ‘ 𝑃 ) ) )
69 65 68 eqtr2d ⊢ ( 𝑅 ∈ CRing → ( ( od ‘ 𝑃 ) ‘ ( 1r ‘ 𝑃 ) ) = ( chr ‘ 𝑅 ) )
70 5 69 eqtr3id ⊢ ( 𝑅 ∈ CRing → ( chr ‘ 𝑃 ) = ( chr ‘ 𝑅 ) )