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

Metamath Proof Explorer

Theorem ply1fermltlchr

Description: Fermat's little theorem for polynomials in a commutative ring F of characteristic P prime: we have the polynomial equation ( X + A ) ^ P = ( ( X ^ P ) + A ) . (Contributed by Thierry Arnoux, 9-Jan-2025)

Ref Expression
Hypotheses ply1fermltlchr.w ⊢ 𝑊 = ( Poly1 ‘ 𝐹 )
ply1fermltlchr.x ⊢ 𝑋 = ( var1 ‘ 𝐹 )
ply1fermltlchr.l ⊢ + = ( +g ‘ 𝑊 )
ply1fermltlchr.n ⊢ 𝑁 = ( mulGrp ‘ 𝑊 )
ply1fermltlchr.t ⊢ ↑ = ( .g ‘ 𝑁 )
ply1fermltlchr.c ⊢ 𝐶 = ( algSc ‘ 𝑊 )
ply1fermltlchr.a ⊢ 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
ply1fermltlchr.p ⊢ 𝑃 = ( chr ‘ 𝐹 )
ply1fermltlchr.f ⊢ ( 𝜑 → 𝐹 ∈ CRing )
ply1fermltlchr.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
ply1fermltlchr.2 ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
Assertion ply1fermltlchr ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ply1fermltlchr.w ⊢ 𝑊 = ( Poly1 ‘ 𝐹 )
2 ply1fermltlchr.x ⊢ 𝑋 = ( var1 ‘ 𝐹 )
3 ply1fermltlchr.l ⊢ + = ( +g ‘ 𝑊 )
4 ply1fermltlchr.n ⊢ 𝑁 = ( mulGrp ‘ 𝑊 )
5 ply1fermltlchr.t ⊢ ↑ = ( .g ‘ 𝑁 )
6 ply1fermltlchr.c ⊢ 𝐶 = ( algSc ‘ 𝑊 )
7 ply1fermltlchr.a ⊢ 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
8 ply1fermltlchr.p ⊢ 𝑃 = ( chr ‘ 𝐹 )
9 ply1fermltlchr.f ⊢ ( 𝜑 → 𝐹 ∈ CRing )
10 ply1fermltlchr.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
11 ply1fermltlchr.2 ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
12 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13 4 fveq2i ⊢ ( .g ‘ 𝑁 ) = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
14 5 13 eqtri ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
15 eqid ⊢ ( chr ‘ 𝑊 ) = ( chr ‘ 𝑊 )
16 1 ply1crng ⊢ ( 𝐹 ∈ CRing → 𝑊 ∈ CRing )
17 9 16 syl ⊢ ( 𝜑 → 𝑊 ∈ CRing )
18 1 ply1chr ⊢ ( 𝐹 ∈ CRing → ( chr ‘ 𝑊 ) = ( chr ‘ 𝐹 ) )
19 9 18 syl ⊢ ( 𝜑 → ( chr ‘ 𝑊 ) = ( chr ‘ 𝐹 ) )
20 19 8 eqtr4di ⊢ ( 𝜑 → ( chr ‘ 𝑊 ) = 𝑃 )
21 20 10 eqeltrd ⊢ ( 𝜑 → ( chr ‘ 𝑊 ) ∈ ℙ )
22 9 crngringd ⊢ ( 𝜑 → 𝐹 ∈ Ring )
23 2 1 12 vr1cl ⊢ ( 𝐹 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
24 22 23 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
25 eqid ⊢ ( ℤRHom ‘ 𝐹 ) = ( ℤRHom ‘ 𝐹 )
26 25 zrhrhm ⊢ ( 𝐹 ∈ Ring → ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) )
27 zringbas ⊢ ℤ = ( Base ‘ ℤring )
28 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
29 27 28 rhmf ⊢ ( ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) → ( ℤRHom ‘ 𝐹 ) : ℤ ⟶ ( Base ‘ 𝐹 ) )
30 22 26 29 3syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐹 ) : ℤ ⟶ ( Base ‘ 𝐹 ) )
31 30 11 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ∈ ( Base ‘ 𝐹 ) )
32 1 6 28 12 ply1sclcl ⊢ ( ( 𝐹 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ∈ ( Base ‘ 𝐹 ) ) → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ∈ ( Base ‘ 𝑊 ) )
33 22 31 32 syl2anc ⊢ ( 𝜑 → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ∈ ( Base ‘ 𝑊 ) )
34 7 33 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑊 ) )
35 12 3 14 15 17 21 24 34 freshmansdream ⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ ( 𝑋 + 𝐴 ) ) = ( ( ( chr ‘ 𝑊 ) ↑ 𝑋 ) + ( ( chr ‘ 𝑊 ) ↑ 𝐴 ) ) )
36 20 oveq1d ⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ ( 𝑋 + 𝐴 ) ) = ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) )
37 20 oveq1d ⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ 𝑋 ) = ( 𝑃 ↑ 𝑋 ) )
38 20 oveq1d ⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ 𝐴 ) = ( 𝑃 ↑ 𝐴 ) )
39 1 ply1assa ⊢ ( 𝐹 ∈ CRing → 𝑊 ∈ AssAlg )
40 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
41 6 40 asclrhm ⊢ ( 𝑊 ∈ AssAlg → 𝐶 ∈ ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
42 9 39 41 3syl ⊢ ( 𝜑 → 𝐶 ∈ ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
43 9 crnggrpd ⊢ ( 𝜑 → 𝐹 ∈ Grp )
44 1 ply1sca ⊢ ( 𝐹 ∈ Grp → 𝐹 = ( Scalar ‘ 𝑊 ) )
45 43 44 syl ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
46 45 oveq1d ⊢ ( 𝜑 → ( 𝐹 RingHom 𝑊 ) = ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
47 42 46 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 RingHom 𝑊 ) )
48 eqid ⊢ ( mulGrp ‘ 𝐹 ) = ( mulGrp ‘ 𝐹 )
49 48 4 rhmmhm ⊢ ( 𝐶 ∈ ( 𝐹 RingHom 𝑊 ) → 𝐶 ∈ ( ( mulGrp ‘ 𝐹 ) MndHom 𝑁 ) )
50 47 49 syl ⊢ ( 𝜑 → 𝐶 ∈ ( ( mulGrp ‘ 𝐹 ) MndHom 𝑁 ) )
51 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
52 nnnn0 ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
53 10 51 52 3syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
54 48 28 mgpbas ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ ( mulGrp ‘ 𝐹 ) )
55 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐹 ) ) = ( .g ‘ ( mulGrp ‘ 𝐹 ) )
56 54 55 5 mhmmulg ⊢ ( ( 𝐶 ∈ ( ( mulGrp ‘ 𝐹 ) MndHom 𝑁 ) ∧ 𝑃 ∈ ℕ0 ∧ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ∈ ( Base ‘ 𝐹 ) ) → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = ( 𝑃 ↑ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) )
57 50 53 31 56 syl3anc ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = ( 𝑃 ↑ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) )
58 7 a1i ⊢ ( 𝜑 → 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
59 58 oveq2d ⊢ ( 𝜑 → ( 𝑃 ↑ 𝐴 ) = ( 𝑃 ↑ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) )
60 57 59 eqtr4d ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = ( 𝑃 ↑ 𝐴 ) )
61 eqid ⊢ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 )
62 8 28 55 61 10 11 9 fermltlchr ⊢ ( 𝜑 → ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
63 62 fveq2d ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
64 63 7 eqtr4di ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = 𝐴 )
65 38 60 64 3eqtr2d ⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ 𝐴 ) = 𝐴 )
66 37 65 oveq12d ⊢ ( 𝜑 → ( ( ( chr ‘ 𝑊 ) ↑ 𝑋 ) + ( ( chr ‘ 𝑊 ) ↑ 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )
67 35 36 66 3eqtr3d ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )