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 = ( Z/nZ ` P )
	ply1fermltl.w	|- W = ( Poly1 ` Z )
	ply1fermltl.x	|- X = ( var1 ` Z )
	ply1fermltl.l	|- .+ = ( +g ` W )
	ply1fermltl.n	|- N = ( mulGrp ` W )
	ply1fermltl.t	|- .^ = ( .g ` N )
	ply1fermltl.c	|- C = ( algSc ` W )
	ply1fermltl.a	|- A = ( C ` ( ( ZRHom ` Z ) ` E ) )
	ply1fermltl.p	|- ( ph -> P e. Prime )
	ply1fermltl.1	|- ( ph -> E e. ZZ )
Assertion	ply1fermltl	|- ( ph -> ( P .^ ( X .+ A ) ) = ( ( P .^ X ) .+ A ) )

Proof

Step	Hyp	Ref	Expression
1		ply1fermltl.z	|- Z = ( Z/nZ ` P )
2		ply1fermltl.w	|- W = ( Poly1 ` Z )
3		ply1fermltl.x	|- X = ( var1 ` Z )
4		ply1fermltl.l	|- .+ = ( +g ` W )
5		ply1fermltl.n	|- N = ( mulGrp ` W )
6		ply1fermltl.t	|- .^ = ( .g ` N )
7		ply1fermltl.c	|- C = ( algSc ` W )
8		ply1fermltl.a	|- A = ( C ` ( ( ZRHom ` Z ) ` E ) )
9		ply1fermltl.p	|- ( ph -> P e. Prime )
10		ply1fermltl.1	|- ( ph -> E e. ZZ )
11		eqid	|- ( chr ` Z ) = ( chr ` Z )
12		prmnn	|- ( P e. Prime -> P e. NN )
13		nnnn0	|- ( P e. NN -> P e. NN0 )
14	1	zncrng	|- ( P e. NN0 -> Z e. CRing )
15	9 12 13 14	4syl	|- ( ph -> Z e. CRing )
16	1	znchr	|- ( P e. NN0 -> ( chr ` Z ) = P )
17	9 12 13 16	4syl	|- ( ph -> ( chr ` Z ) = P )
18	17 9	eqeltrd	|- ( ph -> ( chr ` Z ) e. Prime )
19	2 3 4 5 6 7 8 11 15 18 10	ply1fermltlchr	|- ( ph -> ( ( chr ` Z ) .^ ( X .+ A ) ) = ( ( ( chr ` Z ) .^ X ) .+ A ) )
20	17	oveq1d	|- ( ph -> ( ( chr ` Z ) .^ ( X .+ A ) ) = ( P .^ ( X .+ A ) ) )
21	17	oveq1d	|- ( ph -> ( ( chr ` Z ) .^ X ) = ( P .^ X ) )
22	21	oveq1d	|- ( ph -> ( ( ( chr ` Z ) .^ X ) .+ A ) = ( ( P .^ X ) .+ A ) )
23	19 20 22	3eqtr3d	|- ( ph -> ( P .^ ( X .+ A ) ) = ( ( P .^ X ) .+ A ) )