Theorem ply1fermltlchr

Description: Fermat's little theorem for polynomials in a commutative ring F of characteristic P prime: we have the polynomial equation ( X + A ) ^ P = ( ( X ^ P ) + A ) . (Contributed by Thierry Arnoux, 9-Jan-2025)

	Ref	Expression
Hypotheses	ply1fermltlchr.w	$$⊢W={\mathrm{Poly}}_1\left(F\right)$$
	ply1fermltlchr.x	$$⊢X={\mathrm{var}}_1\left(F\right)$$
	ply1fermltlchr.l	$$⊢\underset{\dot{}}{+}={+}_W$$
	ply1fermltlchr.n	$$⊢N={\mathrm{mulGrp}}_W$$
	ply1fermltlchr.t	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
	ply1fermltlchr.c	$$⊢C=\mathrm{algSc}\left(W\right)$$
	ply1fermltlchr.a	$$⊢A=C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
	ply1fermltlchr.p	$$⊢P=\mathrm{chr}\left(F\right)$$
	ply1fermltlchr.f	$$⊢\phi \to F\in \mathrm{CRing}$$
	ply1fermltlchr.1	$$⊢\phi \to P\in \mathbb{P}$$
	ply1fermltlchr.2	$$⊢\phi \to E\in \mathbb{Z}$$
Assertion	ply1fermltlchr	$$⊢\phi \to P\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)=\left(P\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}A$$

Proof

Step	Hyp	Ref	Expression
1		ply1fermltlchr.w	$$⊢W={\mathrm{Poly}}_1\left(F\right)$$
2		ply1fermltlchr.x	$$⊢X={\mathrm{var}}_1\left(F\right)$$
3		ply1fermltlchr.l	$$⊢\underset{\dot{}}{+}={+}_W$$
4		ply1fermltlchr.n	$$⊢N={\mathrm{mulGrp}}_W$$
5		ply1fermltlchr.t	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
6		ply1fermltlchr.c	$$⊢C=\mathrm{algSc}\left(W\right)$$
7		ply1fermltlchr.a	$$⊢A=C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
8		ply1fermltlchr.p	$$⊢P=\mathrm{chr}\left(F\right)$$
9		ply1fermltlchr.f	$$⊢\phi \to F\in \mathrm{CRing}$$
10		ply1fermltlchr.1	$$⊢\phi \to P\in \mathbb{P}$$
11		ply1fermltlchr.2	$$⊢\phi \to E\in \mathbb{Z}$$
12		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
13	4	fveq2i	$$⊢{\cdot }_N={\cdot }_{{\mathrm{mulGrp}}_W}$$
14	5 13	eqtri	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_W}$$
15		eqid	$$⊢\mathrm{chr}\left(W\right)=\mathrm{chr}\left(W\right)$$
16	1	ply1crng	$$⊢F\in \mathrm{CRing}\to W\in \mathrm{CRing}$$
17	9 16	syl	$$⊢\phi \to W\in \mathrm{CRing}$$
18	1	ply1chr	$$⊢F\in \mathrm{CRing}\to \mathrm{chr}\left(W\right)=\mathrm{chr}\left(F\right)$$
19	9 18	syl	$$⊢\phi \to \mathrm{chr}\left(W\right)=\mathrm{chr}\left(F\right)$$
20	19 8	eqtr4di	$$⊢\phi \to \mathrm{chr}\left(W\right)=P$$
21	20 10	eqeltrd	$$⊢\phi \to \mathrm{chr}\left(W\right)\in \mathbb{P}$$
22	9	crngringd	$$⊢\phi \to F\in \mathrm{Ring}$$
23	2 1 12	vr1cl	$$⊢F\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
24	22 23	syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
25		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(F\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)$$
26	25	zrhrhm	$$⊢F\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}F\right)$$
27		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
28		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
29	27 28	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left(F\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}F\right)\to \mathrm{\mathbb{Z}RHom}\left(F\right):\mathbb{Z}⟶{\mathrm{Base}}_F$$
30	22 26 29	3syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right):\mathbb{Z}⟶{\mathrm{Base}}_F$$
31	30 11	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\in {\mathrm{Base}}_F$$
32	1 6 28 12	ply1sclcl	$$⊢\left(F\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\in {\mathrm{Base}}_F\right)\to C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\in {\mathrm{Base}}_W$$
33	22 31 32	syl2anc	$$⊢\phi \to C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)\in {\mathrm{Base}}_W$$
34	7 33	eqeltrid	$$⊢\phi \to A\in {\mathrm{Base}}_W$$
35	12 3 14 15 17 21 24 34	freshmansdream	$$⊢\phi \to \mathrm{chr}\left(W\right)\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)=\left(\mathrm{chr}\left(W\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\mathrm{chr}\left(W\right)\underset{\dot{}}{\times }A\right)$$
36	20	oveq1d	$$⊢\phi \to \mathrm{chr}\left(W\right)\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)=P\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)$$
37	20	oveq1d	$$⊢\phi \to \mathrm{chr}\left(W\right)\underset{\dot{}}{\times }X=P\underset{\dot{}}{\times }X$$
38	20	oveq1d	$$⊢\phi \to \mathrm{chr}\left(W\right)\underset{\dot{}}{\times }A=P\underset{\dot{}}{\times }A$$
39	1	ply1assa	$$⊢F\in \mathrm{CRing}\to W\in \mathrm{AssAlg}$$
40		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
41	6 40	asclrhm	$$⊢W\in \mathrm{AssAlg}\to C\in \left(\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W\right)$$
42	9 39 41	3syl	$$⊢\phi \to C\in \left(\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W\right)$$
43	9	crnggrpd	$$⊢\phi \to F\in \mathrm{Grp}$$
44	1	ply1sca	$$⊢F\in \mathrm{Grp}\to F=\mathrm{Scalar}\left(W\right)$$
45	43 44	syl	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
46	45	oveq1d	$$⊢\phi \to F\mathrm{RingHom}W=\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W$$
47	42 46	eleqtrrd	$$⊢\phi \to C\in \left(F\mathrm{RingHom}W\right)$$
48		eqid	$$⊢{\mathrm{mulGrp}}_F={\mathrm{mulGrp}}_F$$
49	48 4	rhmmhm	$$⊢C\in \left(F\mathrm{RingHom}W\right)\to C\in \left({\mathrm{mulGrp}}_F\mathrm{MndHom}N\right)$$
50	47 49	syl	$$⊢\phi \to C\in \left({\mathrm{mulGrp}}_F\mathrm{MndHom}N\right)$$
51		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
52		nnnn0	$$⊢P\in \mathbb{N}\to P\in {\mathbb{N}}_0$$
53	10 51 52	3syl	$$⊢\phi \to P\in {\mathbb{N}}_0$$
54	48 28	mgpbas	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_{{\mathrm{mulGrp}}_F}$$
55		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_F}={\cdot }_{{\mathrm{mulGrp}}_F}$$
56	54 55 5	mhmmulg	$$⊢\left(C\in \left({\mathrm{mulGrp}}_F\mathrm{MndHom}N\right)\wedge P\in {\mathbb{N}}_0\wedge \mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\in {\mathrm{Base}}_F\right)\to C\left(P{\cdot }_{{\mathrm{mulGrp}}_F}\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)=P\underset{\dot{}}{\times }C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
57	50 53 31 56	syl3anc	$$⊢\phi \to C\left(P{\cdot }_{{\mathrm{mulGrp}}_F}\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)=P\underset{\dot{}}{\times }C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
58	7	a1i	$$⊢\phi \to A=C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
59	58	oveq2d	$$⊢\phi \to P\underset{\dot{}}{\times }A=P\underset{\dot{}}{\times }C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
60	57 59	eqtr4d	$$⊢\phi \to C\left(P{\cdot }_{{\mathrm{mulGrp}}_F}\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)=P\underset{\dot{}}{\times }A$$
61		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
62	8 28 55 61 10 11 9	fermltlchr	$$⊢\phi \to P{\cdot }_{{\mathrm{mulGrp}}_F}\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)=\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)$$
63	62	fveq2d	$$⊢\phi \to C\left(P{\cdot }_{{\mathrm{mulGrp}}_F}\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)=C\left(\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)$$
64	63 7	eqtr4di	$$⊢\phi \to C\left(P{\cdot }_{{\mathrm{mulGrp}}_F}\mathrm{\mathbb{Z}RHom}\left(F\right)\left(E\right)\right)=A$$
65	38 60 64	3eqtr2d	$$⊢\phi \to \mathrm{chr}\left(W\right)\underset{\dot{}}{\times }A=A$$
66	37 65	oveq12d	$$⊢\phi \to \left(\mathrm{chr}\left(W\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\mathrm{chr}\left(W\right)\underset{\dot{}}{\times }A\right)=\left(P\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}A$$
67	35 36 66	3eqtr3d	$$⊢\phi \to P\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)=\left(P\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}A$$