This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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