Metamath Proof Explorer


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 ( 𝜑 → ( 𝑃 ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 𝑋 ) + 𝐴 ) )