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

Metamath Proof Explorer

Theorem ply1chr

Proof