Theorem ply1fermltl

Description: Fermat's little theorem for polynomials. If P is prime, Then ( X + A ) ^ P = ( ( X ^ P ) + A ) modulo P . (Contributed by Thierry Arnoux, 24-Jul-2024)

	Ref	Expression
Hypotheses	ply1fermltl.z	$$⊢Z=\mathbb{Z}/P\mathbb{Z}$$
	ply1fermltl.w	$$⊢W={\mathrm{Poly}}_1\left(Z\right)$$
	ply1fermltl.x	$$⊢X={\mathrm{var}}_1\left(Z\right)$$
	ply1fermltl.l	$$⊢\underset{\dot{}}{+}={+}_W$$
	ply1fermltl.n	$$⊢N={\mathrm{mulGrp}}_W$$
	ply1fermltl.t	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
	ply1fermltl.c	$$⊢C=\mathrm{algSc}\left(W\right)$$
	ply1fermltl.a	$$⊢A=C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)$$
	ply1fermltl.p	$$⊢\phi \to P\in \mathbb{P}$$
	ply1fermltl.1	$$⊢\phi \to E\in \mathbb{Z}$$
Assertion	ply1fermltl	$$⊢\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		ply1fermltl.z	$$⊢Z=\mathbb{Z}/P\mathbb{Z}$$
2		ply1fermltl.w	$$⊢W={\mathrm{Poly}}_1\left(Z\right)$$
3		ply1fermltl.x	$$⊢X={\mathrm{var}}_1\left(Z\right)$$
4		ply1fermltl.l	$$⊢\underset{\dot{}}{+}={+}_W$$
5		ply1fermltl.n	$$⊢N={\mathrm{mulGrp}}_W$$
6		ply1fermltl.t	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
7		ply1fermltl.c	$$⊢C=\mathrm{algSc}\left(W\right)$$
8		ply1fermltl.a	$$⊢A=C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)$$
9		ply1fermltl.p	$$⊢\phi \to P\in \mathbb{P}$$
10		ply1fermltl.1	$$⊢\phi \to E\in \mathbb{Z}$$
11		eqid	$$⊢\mathrm{chr}\left(Z\right)=\mathrm{chr}\left(Z\right)$$
12		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
13		nnnn0	$$⊢P\in \mathbb{N}\to P\in {\mathbb{N}}_0$$
14	1	zncrng	$$⊢P\in {\mathbb{N}}_0\to Z\in \mathrm{CRing}$$
15	9 12 13 14	4syl	$$⊢\phi \to Z\in \mathrm{CRing}$$
16	1	znchr	$$⊢P\in {\mathbb{N}}_0\to \mathrm{chr}\left(Z\right)=P$$
17	9 12 13 16	4syl	$$⊢\phi \to \mathrm{chr}\left(Z\right)=P$$
18	17 9	eqeltrd	$$⊢\phi \to \mathrm{chr}\left(Z\right)\in \mathbb{P}$$
19	2 3 4 5 6 7 8 11 15 18 10	ply1fermltlchr	$$⊢\phi \to \mathrm{chr}\left(Z\right)\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)=\left(\mathrm{chr}\left(Z\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}A$$
20	17	oveq1d	$$⊢\phi \to \mathrm{chr}\left(Z\right)\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)=P\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)$$
21	17	oveq1d	$$⊢\phi \to \mathrm{chr}\left(Z\right)\underset{\dot{}}{\times }X=P\underset{\dot{}}{\times }X$$
22	21	oveq1d	$$⊢\phi \to \left(\mathrm{chr}\left(Z\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}A=\left(P\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}A$$
23	19 20 22	3eqtr3d	$$⊢\phi \to P\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)=\left(P\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}A$$