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{Base}}_W={\mathrm{Base}}_W$$
12	5	fveq2i	$$⊢{\cdot }_N={\cdot }_{{\mathrm{mulGrp}}_W}$$
13	6 12	eqtri	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_W}$$
14		eqid	$$⊢\mathrm{chr}\left(W\right)=\mathrm{chr}\left(W\right)$$
15		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
16		nnnn0	$$⊢P\in \mathbb{N}\to P\in {\mathbb{N}}_0$$
17	1	zncrng	$$⊢P\in {\mathbb{N}}_0\to Z\in \mathrm{CRing}$$
18	9 15 16 17	4syl	$$⊢\phi \to Z\in \mathrm{CRing}$$
19	2	ply1crng	$$⊢Z\in \mathrm{CRing}\to W\in \mathrm{CRing}$$
20	18 19	syl	$$⊢\phi \to W\in \mathrm{CRing}$$
21	2	ply1chr	$$⊢Z\in \mathrm{CRing}\to \mathrm{chr}\left(W\right)=\mathrm{chr}\left(Z\right)$$
22	18 21	syl	$$⊢\phi \to \mathrm{chr}\left(W\right)=\mathrm{chr}\left(Z\right)$$
23	1	znchr	$$⊢P\in {\mathbb{N}}_0\to \mathrm{chr}\left(Z\right)=P$$
24	9 15 16 23	4syl	$$⊢\phi \to \mathrm{chr}\left(Z\right)=P$$
25	22 24	eqtrd	$$⊢\phi \to \mathrm{chr}\left(W\right)=P$$
26	25 9	eqeltrd	$$⊢\phi \to \mathrm{chr}\left(W\right)\in \mathbb{P}$$
27	18	crngringd	$$⊢\phi \to Z\in \mathrm{Ring}$$
28	3 2 11	vr1cl	$$⊢Z\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
29	27 28	syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
30		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(Z\right)=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
31	30	zrhrhm	$$⊢Z\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(Z\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Z\right)$$
32		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
33		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
34	32 33	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left(Z\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Z\right)\to \mathrm{\mathbb{Z}RHom}\left(Z\right):\mathbb{Z}⟶{\mathrm{Base}}_Z$$
35	27 31 34	3syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(Z\right):\mathbb{Z}⟶{\mathrm{Base}}_Z$$
36	35 10	ffvelrnd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\in {\mathrm{Base}}_Z$$
37	2 7 33 11	ply1sclcl	$$⊢\left(Z\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\in {\mathrm{Base}}_Z\right)\to C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)\in {\mathrm{Base}}_W$$
38	27 36 37	syl2anc	$$⊢\phi \to C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)\in {\mathrm{Base}}_W$$
39	8 38	eqeltrid	$$⊢\phi \to A\in {\mathrm{Base}}_W$$
40	11 4 13 14 20 26 29 39	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)$$
41	25	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)$$
42	25	oveq1d	$$⊢\phi \to \mathrm{chr}\left(W\right)\underset{\dot{}}{\times }X=P\underset{\dot{}}{\times }X$$
43	25	oveq1d	$$⊢\phi \to \mathrm{chr}\left(W\right)\underset{\dot{}}{\times }A=P\underset{\dot{}}{\times }A$$
44	2	ply1assa	$$⊢Z\in \mathrm{CRing}\to W\in \mathrm{AssAlg}$$
45		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
46	7 45	asclrhm	$$⊢W\in \mathrm{AssAlg}\to C\in \left(\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W\right)$$
47	18 44 46	3syl	$$⊢\phi \to C\in \left(\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W\right)$$
48	18	crnggrpd	$$⊢\phi \to Z\in \mathrm{Grp}$$
49	2	ply1sca	$$⊢Z\in \mathrm{Grp}\to Z=\mathrm{Scalar}\left(W\right)$$
50	48 49	syl	$$⊢\phi \to Z=\mathrm{Scalar}\left(W\right)$$
51	50	oveq1d	$$⊢\phi \to Z\mathrm{RingHom}W=\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W$$
52	47 51	eleqtrrd	$$⊢\phi \to C\in \left(Z\mathrm{RingHom}W\right)$$
53		eqid	$$⊢{\mathrm{mulGrp}}_Z={\mathrm{mulGrp}}_Z$$
54	53 5	rhmmhm	$$⊢C\in \left(Z\mathrm{RingHom}W\right)\to C\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}N\right)$$
55	52 54	syl	$$⊢\phi \to C\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}N\right)$$
56	9 15 16	3syl	$$⊢\phi \to P\in {\mathbb{N}}_0$$
57	53 33	mgpbas	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}$$
58		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_Z}={\cdot }_{{\mathrm{mulGrp}}_Z}$$
59	57 58 6	mhmmulg	$$⊢\left(C\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}N\right)\wedge P\in {\mathbb{N}}_0\wedge \mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\in {\mathrm{Base}}_Z\right)\to C\left(P{\cdot }_{{\mathrm{mulGrp}}_Z}\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)=P\underset{\dot{}}{\times }C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)$$
60	55 56 36 59	syl3anc	$$⊢\phi \to C\left(P{\cdot }_{{\mathrm{mulGrp}}_Z}\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)=P\underset{\dot{}}{\times }C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)$$
61	8	a1i	$$⊢\phi \to A=C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)$$
62	61	oveq2d	$$⊢\phi \to P\underset{\dot{}}{\times }A=P\underset{\dot{}}{\times }C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)$$
63	60 62	eqtr4d	$$⊢\phi \to C\left(P{\cdot }_{{\mathrm{mulGrp}}_Z}\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)=P\underset{\dot{}}{\times }A$$
64	1 33 58	znfermltl	$$⊢\left(P\in \mathbb{P}\wedge \mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\in {\mathrm{Base}}_Z\right)\to P{\cdot }_{{\mathrm{mulGrp}}_Z}\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)=\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)$$
65	9 36 64	syl2anc	$$⊢\phi \to P{\cdot }_{{\mathrm{mulGrp}}_Z}\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)=\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)$$
66	65	fveq2d	$$⊢\phi \to C\left(P{\cdot }_{{\mathrm{mulGrp}}_Z}\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)=C\left(\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)$$
67	66 8	eqtr4di	$$⊢\phi \to C\left(P{\cdot }_{{\mathrm{mulGrp}}_Z}\mathrm{\mathbb{Z}RHom}\left(Z\right)\left(E\right)\right)=A$$
68	43 63 67	3eqtr2d	$$⊢\phi \to \mathrm{chr}\left(W\right)\underset{\dot{}}{\times }A=A$$
69	42 68	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$$
70	40 41 69	3eqtr3d	$$⊢\phi \to P\underset{\dot{}}{\times }\left(X\underset{\dot{}}{+}A\right)=\left(P\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}A$$