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	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑃 )
	ply1fermltl.w	⊢ 𝑊 = ( Poly1 ‘ 𝑍 )
	ply1fermltl.x	⊢ 𝑋 = ( var1 ‘ 𝑍 )
	ply1fermltl.l	⊢ + = ( +g ‘ 𝑊 )
	ply1fermltl.n	⊢ 𝑁 = ( mulGrp ‘ 𝑊 )
	ply1fermltl.t	⊢ ↑ = ( .g ‘ 𝑁 )
	ply1fermltl.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
	ply1fermltl.a	⊢ 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝐸 ) )
	ply1fermltl.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	ply1fermltl.1	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
Assertion	ply1fermltl	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1fermltl.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑃 )
2		ply1fermltl.w	⊢ 𝑊 = ( Poly1 ‘ 𝑍 )
3		ply1fermltl.x	⊢ 𝑋 = ( var1 ‘ 𝑍 )
4		ply1fermltl.l	⊢ + = ( +g ‘ 𝑊 )
5		ply1fermltl.n	⊢ 𝑁 = ( mulGrp ‘ 𝑊 )
6		ply1fermltl.t	⊢ ↑ = ( .g ‘ 𝑁 )
7		ply1fermltl.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
8		ply1fermltl.a	⊢ 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝐸 ) )
9		ply1fermltl.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
10		ply1fermltl.1	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
11		eqid	⊢ ( chr ‘ 𝑍 ) = ( chr ‘ 𝑍 )
12		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
13		nnnn0	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
14	1	zncrng	⊢ ( 𝑃 ∈ ℕ0 → 𝑍 ∈ CRing )
15	9 12 13 14	4syl	⊢ ( 𝜑 → 𝑍 ∈ CRing )
16	1	znchr	⊢ ( 𝑃 ∈ ℕ0 → ( chr ‘ 𝑍 ) = 𝑃 )
17	9 12 13 16	4syl	⊢ ( 𝜑 → ( chr ‘ 𝑍 ) = 𝑃 )
18	17 9	eqeltrd	⊢ ( 𝜑 → ( chr ‘ 𝑍 ) ∈ ℙ )
19	2 3 4 5 6 7 8 11 15 18 10	ply1fermltlchr	⊢ ( 𝜑 → ( ( chr ‘ 𝑍 ) ↑ ( 𝑋 + 𝐴 ) ) = ( ( ( chr ‘ 𝑍 ) ↑ 𝑋 ) + 𝐴 ) )
20	17	oveq1d	⊢ ( 𝜑 → ( ( chr ‘ 𝑍 ) ↑ ( 𝑋 + 𝐴 ) ) = ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) )
21	17	oveq1d	⊢ ( 𝜑 → ( ( chr ‘ 𝑍 ) ↑ 𝑋 ) = ( 𝑃 ↑ 𝑋 ) )
22	21	oveq1d	⊢ ( 𝜑 → ( ( ( chr ‘ 𝑍 ) ↑ 𝑋 ) + 𝐴 ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )
23	19 20 22	3eqtr3d	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )