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 \in CRing \to 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 \in CRing \to R \in CRing$
12	11	crnggrpd	$⊢ R \in CRing \to R \in Grp$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15	14 7	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
16	13 15	syl	$⊢ R \in CRing \to 1_{R} \in {Base}_{R}$
17	8	chrcl	$⊢ R \in Ring \to chr (R) \in ℕ_{0}$
18	13 17	syl	$⊢ R \in CRing \to chr (R) \in ℕ_{0}$
19		eqid	$⊢ \cdot_{R} = \cdot_{R}$
20		eqid	$⊢ 0_{R} = 0_{R}$
21	14 6 19 20	odeq	$⊢ (R \in Grp \land 1_{R} \in {Base}_{R} \land chr (R) \in ℕ_{0}) \to (chr (R) = od (R) (1_{R}) \leftrightarrow \forall n \in ℕ_{0} (chr (R) ∥ n \leftrightarrow n \cdot_{R} 1_{R} = 0_{R}))$
22	12 16 18 21	syl3anc	$⊢ R \in CRing \to (chr (R) = od (R) (1_{R}) \leftrightarrow \forall n \in ℕ_{0} (chr (R) ∥ n \leftrightarrow n \cdot_{R} 1_{R} = 0_{R}))$
23	10 22	mpbii	$⊢ R \in CRing \to \forall n \in ℕ_{0} (chr (R) ∥ n \leftrightarrow n \cdot_{R} 1_{R} = 0_{R})$
24	23	r19.21bi	$⊢ (R \in CRing \land n \in ℕ_{0}) \to (chr (R) ∥ n \leftrightarrow n \cdot_{R} 1_{R} = 0_{R})$
25		eqid	$⊢ algSc (P) = algSc (P)$
26	13	adantr	$⊢ (R \in CRing \land n \in ℕ_{0}) \to R \in Ring$
27	12	grpmndd	$⊢ R \in CRing \to R \in Mnd$
28	27	adantr	$⊢ (R \in CRing \land n \in ℕ_{0}) \to R \in Mnd$
29		simpr	$⊢ (R \in CRing \land n \in ℕ_{0}) \to n \in ℕ_{0}$
30	16	adantr	$⊢ (R \in CRing \land n \in ℕ_{0}) \to 1_{R} \in {Base}_{R}$
31	14 19	mulgnn0cl	$⊢ (R \in Mnd \land n \in ℕ_{0} \land 1_{R} \in {Base}_{R}) \to n \cdot_{R} 1_{R} \in {Base}_{R}$
32	28 29 30 31	syl3anc	$⊢ (R \in CRing \land n \in ℕ_{0}) \to n \cdot_{R} 1_{R} \in {Base}_{R}$
33		simpl	$⊢ (R \in CRing \land n \in ℕ_{0}) \to R \in CRing$
34	14 20	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
35	33 13 34	3syl	$⊢ (R \in CRing \land n \in ℕ_{0}) \to 0_{R} \in {Base}_{R}$
36	1 14 25 26 32 35	ply1scleq	$⊢ (R \in CRing \land n \in ℕ_{0}) \to (algSc (P) (n \cdot_{R} 1_{R}) = algSc (P) (0_{R}) \leftrightarrow n \cdot_{R} 1_{R} = 0_{R})$
37	1	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
38	37	adantr	$⊢ (R \in CRing \land n \in ℕ_{0}) \to R = Scalar (P)$
39	38	fveq2d	$⊢ (R \in CRing \land n \in ℕ_{0}) \to \cdot_{R} = \cdot_{Scalar (P)}$
40	39	oveqd	$⊢ (R \in CRing \land n \in ℕ_{0}) \to n \cdot_{R} 1_{R} = n \cdot_{Scalar (P)} 1_{R}$
41	40	fveq2d	$⊢ (R \in CRing \land n \in ℕ_{0}) \to algSc (P) (n \cdot_{R} 1_{R}) = algSc (P) (n \cdot_{Scalar (P)} 1_{R})$
42	1	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
43	42	adantr	$⊢ (R \in CRing \land n \in ℕ_{0}) \to P \in AssAlg$
44	38	fveq2d	$⊢ (R \in CRing \land n \in ℕ_{0}) \to {Base}_{R} = {Base}_{Scalar (P)}$
45	30 44	eleqtrd	$⊢ (R \in CRing \land n \in ℕ_{0}) \to 1_{R} \in {Base}_{Scalar (P)}$
46		eqid	$⊢ Scalar (P) = Scalar (P)$
47		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
48		eqid	$⊢ \cdot_{P} = \cdot_{P}$
49		eqid	$⊢ \cdot_{Scalar (P)} = \cdot_{Scalar (P)}$
50	25 46 47 48 49	asclmulg	$⊢ (P \in AssAlg \land n \in ℕ_{0} \land 1_{R} \in {Base}_{Scalar (P)}) \to algSc (P) (n \cdot_{Scalar (P)} 1_{R}) = n \cdot_{P} algSc (P) (1_{R})$
51	43 29 45 50	syl3anc	$⊢ (R \in CRing \land n \in ℕ_{0}) \to algSc (P) (n \cdot_{Scalar (P)} 1_{R}) = n \cdot_{P} algSc (P) (1_{R})$
52	41 51	eqtrd	$⊢ (R \in CRing \land n \in ℕ_{0}) \to algSc (P) (n \cdot_{R} 1_{R}) = n \cdot_{P} algSc (P) (1_{R})$
53		eqid	$⊢ 0_{P} = 0_{P}$
54	1 25 20 53	ply1scl0	$⊢ R \in Ring \to algSc (P) (0_{R}) = 0_{P}$
55	33 13 54	3syl	$⊢ (R \in CRing \land n \in ℕ_{0}) \to algSc (P) (0_{R}) = 0_{P}$
56	52 55	eqeq12d	$⊢ (R \in CRing \land n \in ℕ_{0}) \to (algSc (P) (n \cdot_{R} 1_{R}) = algSc (P) (0_{R}) \leftrightarrow n \cdot_{P} algSc (P) (1_{R}) = 0_{P})$
57	24 36 56	3bitr2d	$⊢ (R \in CRing \land n \in ℕ_{0}) \to (chr (R) ∥ n \leftrightarrow n \cdot_{P} algSc (P) (1_{R}) = 0_{P})$
58	57	ralrimiva	$⊢ R \in CRing \to \forall n \in ℕ_{0} (chr (R) ∥ n \leftrightarrow n \cdot_{P} algSc (P) (1_{R}) = 0_{P})$
59	1	ply1crng	$⊢ R \in CRing \to P \in CRing$
60	59	crnggrpd	$⊢ R \in CRing \to P \in Grp$
61		eqid	$⊢ {Base}_{P} = {Base}_{P}$
62	1 25 14 61	ply1sclcl	$⊢ (R \in Ring \land 1_{R} \in {Base}_{R}) \to algSc (P) (1_{R}) \in {Base}_{P}$
63	13 16 62	syl2anc	$⊢ R \in CRing \to algSc (P) (1_{R}) \in {Base}_{P}$
64	61 2 48 53	odeq	$⊢ (P \in Grp \land algSc (P) (1_{R}) \in {Base}_{P} \land chr (R) \in ℕ_{0}) \to (chr (R) = od (P) (algSc (P) (1_{R})) \leftrightarrow \forall n \in ℕ_{0} (chr (R) ∥ n \leftrightarrow n \cdot_{P} algSc (P) (1_{R}) = 0_{P}))$
65	60 63 18 64	syl3anc	$⊢ R \in CRing \to (chr (R) = od (P) (algSc (P) (1_{R})) \leftrightarrow \forall n \in ℕ_{0} (chr (R) ∥ n \leftrightarrow n \cdot_{P} algSc (P) (1_{R}) = 0_{P}))$
66	58 65	mpbird	$⊢ R \in CRing \to chr (R) = od (P) (algSc (P) (1_{R}))$
67	1 25 7 3	ply1scl1	$⊢ R \in Ring \to algSc (P) (1_{R}) = 1_{P}$
68	67	fveq2d	$⊢ R \in Ring \to od (P) (algSc (P) (1_{R})) = od (P) (1_{P})$
69	13 68	syl	$⊢ R \in CRing \to od (P) (algSc (P) (1_{R})) = od (P) (1_{P})$
70	66 69	eqtr2d	$⊢ R \in CRing \to od (P) (1_{P}) = chr (R)$
71	5 70	eqtr3id	$⊢ R \in CRing \to chr (P) = chr (R)$

Metamath Proof Explorer

Theorem ply1chr

Proof