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 
|- Z = ( Z/nZ ` P )
ply1fermltl.w 
|- W = ( Poly1 ` Z )
ply1fermltl.x 
|- X = ( var1 ` Z )
ply1fermltl.l 
|- .+ = ( +g ` W )
ply1fermltl.n 
|- N = ( mulGrp ` W )
ply1fermltl.t 
|- .^ = ( .g ` N )
ply1fermltl.c 
|- C = ( algSc ` W )
ply1fermltl.a 
|- A = ( C ` ( ( ZRHom ` Z ) ` E ) )
ply1fermltl.p 
|- ( ph -> P e. Prime )
ply1fermltl.1 
|- ( ph -> E e. ZZ )
Assertion ply1fermltl 
|- ( ph -> ( P .^ ( X .+ A ) ) = ( ( P .^ X ) .+ A ) )

Proof

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