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 
|- W = ( Poly1 ` F )
ply1fermltlchr.x 
|- X = ( var1 ` F )
ply1fermltlchr.l 
|- .+ = ( +g ` W )
ply1fermltlchr.n 
|- N = ( mulGrp ` W )
ply1fermltlchr.t 
|- .^ = ( .g ` N )
ply1fermltlchr.c 
|- C = ( algSc ` W )
ply1fermltlchr.a 
|- A = ( C ` ( ( ZRHom ` F ) ` E ) )
ply1fermltlchr.p 
|- P = ( chr ` F )
ply1fermltlchr.f 
|- ( ph -> F e. CRing )
ply1fermltlchr.1 
|- ( ph -> P e. Prime )
ply1fermltlchr.2 
|- ( ph -> E e. ZZ )
Assertion ply1fermltlchr 
|- ( ph -> ( P .^ ( X .+ A ) ) = ( ( P .^ X ) .+ A ) )

Proof

Step Hyp Ref Expression
1 ply1fermltlchr.w 
 |-  W = ( Poly1 ` F )
2 ply1fermltlchr.x 
 |-  X = ( var1 ` F )
3 ply1fermltlchr.l 
 |-  .+ = ( +g ` W )
4 ply1fermltlchr.n 
 |-  N = ( mulGrp ` W )
5 ply1fermltlchr.t 
 |-  .^ = ( .g ` N )
6 ply1fermltlchr.c 
 |-  C = ( algSc ` W )
7 ply1fermltlchr.a 
 |-  A = ( C ` ( ( ZRHom ` F ) ` E ) )
8 ply1fermltlchr.p 
 |-  P = ( chr ` F )
9 ply1fermltlchr.f 
 |-  ( ph -> F e. CRing )
10 ply1fermltlchr.1 
 |-  ( ph -> P e. Prime )
11 ply1fermltlchr.2 
 |-  ( ph -> E e. ZZ )
12 eqid 
 |-  ( Base ` W ) = ( Base ` W )
13 4 fveq2i 
 |-  ( .g ` N ) = ( .g ` ( mulGrp ` W ) )
14 5 13 eqtri 
 |-  .^ = ( .g ` ( mulGrp ` W ) )
15 eqid 
 |-  ( chr ` W ) = ( chr ` W )
16 1 ply1crng 
 |-  ( F e. CRing -> W e. CRing )
17 9 16 syl 
 |-  ( ph -> W e. CRing )
18 1 ply1chr 
 |-  ( F e. CRing -> ( chr ` W ) = ( chr ` F ) )
19 9 18 syl 
 |-  ( ph -> ( chr ` W ) = ( chr ` F ) )
20 19 8 eqtr4di 
 |-  ( ph -> ( chr ` W ) = P )
21 20 10 eqeltrd 
 |-  ( ph -> ( chr ` W ) e. Prime )
22 9 crngringd 
 |-  ( ph -> F e. Ring )
23 2 1 12 vr1cl 
 |-  ( F e. Ring -> X e. ( Base ` W ) )
24 22 23 syl 
 |-  ( ph -> X e. ( Base ` W ) )
25 eqid 
 |-  ( ZRHom ` F ) = ( ZRHom ` F )
26 25 zrhrhm 
 |-  ( F e. Ring -> ( ZRHom ` F ) e. ( ZZring RingHom F ) )
27 zringbas 
 |-  ZZ = ( Base ` ZZring )
28 eqid 
 |-  ( Base ` F ) = ( Base ` F )
29 27 28 rhmf 
 |-  ( ( ZRHom ` F ) e. ( ZZring RingHom F ) -> ( ZRHom ` F ) : ZZ --> ( Base ` F ) )
30 22 26 29 3syl 
 |-  ( ph -> ( ZRHom ` F ) : ZZ --> ( Base ` F ) )
31 30 11 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` F ) ` E ) e. ( Base ` F ) )
32 1 6 28 12 ply1sclcl 
 |-  ( ( F e. Ring /\ ( ( ZRHom ` F ) ` E ) e. ( Base ` F ) ) -> ( C ` ( ( ZRHom ` F ) ` E ) ) e. ( Base ` W ) )
33 22 31 32 syl2anc 
 |-  ( ph -> ( C ` ( ( ZRHom ` F ) ` E ) ) e. ( Base ` W ) )
34 7 33 eqeltrid 
 |-  ( ph -> A e. ( Base ` W ) )
35 12 3 14 15 17 21 24 34 freshmansdream 
 |-  ( ph -> ( ( chr ` W ) .^ ( X .+ A ) ) = ( ( ( chr ` W ) .^ X ) .+ ( ( chr ` W ) .^ A ) ) )
36 20 oveq1d 
 |-  ( ph -> ( ( chr ` W ) .^ ( X .+ A ) ) = ( P .^ ( X .+ A ) ) )
37 20 oveq1d 
 |-  ( ph -> ( ( chr ` W ) .^ X ) = ( P .^ X ) )
38 20 oveq1d 
 |-  ( ph -> ( ( chr ` W ) .^ A ) = ( P .^ A ) )
39 1 ply1assa 
 |-  ( F e. CRing -> W e. AssAlg )
40 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
41 6 40 asclrhm 
 |-  ( W e. AssAlg -> C e. ( ( Scalar ` W ) RingHom W ) )
42 9 39 41 3syl 
 |-  ( ph -> C e. ( ( Scalar ` W ) RingHom W ) )
43 9 crnggrpd 
 |-  ( ph -> F e. Grp )
44 1 ply1sca 
 |-  ( F e. Grp -> F = ( Scalar ` W ) )
45 43 44 syl 
 |-  ( ph -> F = ( Scalar ` W ) )
46 45 oveq1d 
 |-  ( ph -> ( F RingHom W ) = ( ( Scalar ` W ) RingHom W ) )
47 42 46 eleqtrrd 
 |-  ( ph -> C e. ( F RingHom W ) )
48 eqid 
 |-  ( mulGrp ` F ) = ( mulGrp ` F )
49 48 4 rhmmhm 
 |-  ( C e. ( F RingHom W ) -> C e. ( ( mulGrp ` F ) MndHom N ) )
50 47 49 syl 
 |-  ( ph -> C e. ( ( mulGrp ` F ) MndHom N ) )
51 prmnn 
 |-  ( P e. Prime -> P e. NN )
52 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
53 10 51 52 3syl 
 |-  ( ph -> P e. NN0 )
54 48 28 mgpbas 
 |-  ( Base ` F ) = ( Base ` ( mulGrp ` F ) )
55 eqid 
 |-  ( .g ` ( mulGrp ` F ) ) = ( .g ` ( mulGrp ` F ) )
56 54 55 5 mhmmulg 
 |-  ( ( C e. ( ( mulGrp ` F ) MndHom N ) /\ P e. NN0 /\ ( ( ZRHom ` F ) ` E ) e. ( Base ` F ) ) -> ( C ` ( P ( .g ` ( mulGrp ` F ) ) ( ( ZRHom ` F ) ` E ) ) ) = ( P .^ ( C ` ( ( ZRHom ` F ) ` E ) ) ) )
57 50 53 31 56 syl3anc 
 |-  ( ph -> ( C ` ( P ( .g ` ( mulGrp ` F ) ) ( ( ZRHom ` F ) ` E ) ) ) = ( P .^ ( C ` ( ( ZRHom ` F ) ` E ) ) ) )
58 7 a1i 
 |-  ( ph -> A = ( C ` ( ( ZRHom ` F ) ` E ) ) )
59 58 oveq2d 
 |-  ( ph -> ( P .^ A ) = ( P .^ ( C ` ( ( ZRHom ` F ) ` E ) ) ) )
60 57 59 eqtr4d 
 |-  ( ph -> ( C ` ( P ( .g ` ( mulGrp ` F ) ) ( ( ZRHom ` F ) ` E ) ) ) = ( P .^ A ) )
61 eqid 
 |-  ( ( ZRHom ` F ) ` E ) = ( ( ZRHom ` F ) ` E )
62 8 28 55 61 10 11 9 fermltlchr 
 |-  ( ph -> ( P ( .g ` ( mulGrp ` F ) ) ( ( ZRHom ` F ) ` E ) ) = ( ( ZRHom ` F ) ` E ) )
63 62 fveq2d 
 |-  ( ph -> ( C ` ( P ( .g ` ( mulGrp ` F ) ) ( ( ZRHom ` F ) ` E ) ) ) = ( C ` ( ( ZRHom ` F ) ` E ) ) )
64 63 7 eqtr4di 
 |-  ( ph -> ( C ` ( P ( .g ` ( mulGrp ` F ) ) ( ( ZRHom ` F ) ` E ) ) ) = A )
65 38 60 64 3eqtr2d 
 |-  ( ph -> ( ( chr ` W ) .^ A ) = A )
66 37 65 oveq12d 
 |-  ( ph -> ( ( ( chr ` W ) .^ X ) .+ ( ( chr ` W ) .^ A ) ) = ( ( P .^ X ) .+ A ) )
67 35 36 66 3eqtr3d 
 |-  ( ph -> ( P .^ ( X .+ A ) ) = ( ( P .^ X ) .+ A ) )