Metamath Proof Explorer

Theorem fermltlchr

Description: A generalization of Fermat's little theorem in a commutative ring F of prime characteristic. See fermltl . (Contributed by Thierry Arnoux, 9-Jan-2024)

Ref Expression
Hypotheses fermltlchr.z 
|- P = ( chr ` F )
fermltlchr.b 
|- B = ( Base ` F )
fermltlchr.p 
|- .^ = ( .g ` ( mulGrp ` F ) )
fermltlchr.1 
|- A = ( ( ZRHom ` F ) ` E )
fermltlchr.2 
|- ( ph -> P e. Prime )
fermltlchr.3 
|- ( ph -> E e. ZZ )
fermltlchr.4 
|- ( ph -> F e. CRing )
Assertion fermltlchr 
|- ( ph -> ( P .^ A ) = A )

Proof

Step Hyp Ref Expression
1 fermltlchr.z 
 |-  P = ( chr ` F )
2 fermltlchr.b 
 |-  B = ( Base ` F )
3 fermltlchr.p 
 |-  .^ = ( .g ` ( mulGrp ` F ) )
4 fermltlchr.1 
 |-  A = ( ( ZRHom ` F ) ` E )
5 fermltlchr.2 
 |-  ( ph -> P e. Prime )
6 fermltlchr.3 
 |-  ( ph -> E e. ZZ )
7 fermltlchr.4 
 |-  ( ph -> F e. CRing )
8 prmnn 
 |-  ( P e. Prime -> P e. NN )
9 8 nnnn0d 
 |-  ( P e. Prime -> P e. NN0 )
10 5 9 syl 
 |-  ( ph -> P e. NN0 )
11 10 adantr 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> P e. NN0 )
12 6 adantr 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> E e. ZZ )
13 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( ( mulGrp ` CCfld ) |`s ZZ )
14 zsscn 
 |-  ZZ C_ CC
15 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
16 cnfldbas 
 |-  CC = ( Base ` CCfld )
17 15 16 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
18 14 17 sseqtri 
 |-  ZZ C_ ( Base ` ( mulGrp ` CCfld ) )
19 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
20 eqid 
 |-  ( invg ` ( mulGrp ` CCfld ) ) = ( invg ` ( mulGrp ` CCfld ) )
21 cnring 
 |-  CCfld e. Ring
22 15 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
23 21 22 ax-mp 
 |-  ( mulGrp ` CCfld ) e. Mnd
24 cnfld1 
 |-  1 = ( 1r ` CCfld )
25 15 24 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
26 1z 
 |-  1 e. ZZ
27 25 26 eqeltrri 
 |-  ( 0g ` ( mulGrp ` CCfld ) ) e. ZZ
28 eqid 
 |-  ( 0g ` ( mulGrp ` CCfld ) ) = ( 0g ` ( mulGrp ` CCfld ) )
29 13 17 28 ress0g 
 |-  ( ( ( mulGrp ` CCfld ) e. Mnd /\ ( 0g ` ( mulGrp ` CCfld ) ) e. ZZ /\ ZZ C_ CC ) -> ( 0g ` ( mulGrp ` CCfld ) ) = ( 0g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) )
30 23 27 14 29 mp3an 
 |-  ( 0g ` ( mulGrp ` CCfld ) ) = ( 0g ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
31 13 18 19 20 30 ressmulgnn0 
 |-  ( ( P e. NN0 /\ E e. ZZ ) -> ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) E ) = ( P ( .g ` ( mulGrp ` CCfld ) ) E ) )
32 11 12 31 syl2anc 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) E ) = ( P ( .g ` ( mulGrp ` CCfld ) ) E ) )
33 12 zcnd 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> E e. CC )
34 cnfldexp 
 |-  ( ( E e. CC /\ P e. NN0 ) -> ( P ( .g ` ( mulGrp ` CCfld ) ) E ) = ( E ^ P ) )
35 33 11 34 syl2anc 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( P ( .g ` ( mulGrp ` CCfld ) ) E ) = ( E ^ P ) )
36 32 35 eqtrd 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) E ) = ( E ^ P ) )
37 36 fveq2d 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( ( ZRHom ` F ) ` ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) E ) ) = ( ( ZRHom ` F ) ` ( E ^ P ) ) )
38 7 crngringd 
 |-  ( ph -> F e. Ring )
39 eqid 
 |-  ( ZRHom ` F ) = ( ZRHom ` F )
40 39 zrhrhm 
 |-  ( F e. Ring -> ( ZRHom ` F ) e. ( ZZring RingHom F ) )
41 38 40 syl 
 |-  ( ph -> ( ZRHom ` F ) e. ( ZZring RingHom F ) )
42 zringmpg 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring )
43 eqid 
 |-  ( mulGrp ` F ) = ( mulGrp ` F )
44 42 43 rhmmhm 
 |-  ( ( ZRHom ` F ) e. ( ZZring RingHom F ) -> ( ZRHom ` F ) e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` F ) ) )
45 41 44 syl 
 |-  ( ph -> ( ZRHom ` F ) e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` F ) ) )
46 45 adantr 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( ZRHom ` F ) e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` F ) ) )
47 13 17 ressbas2 
 |-  ( ZZ C_ CC -> ZZ = ( Base ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) )
48 14 47 ax-mp 
 |-  ZZ = ( Base ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
49 eqid 
 |-  ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) = ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
50 48 49 3 mhmmulg 
 |-  ( ( ( ZRHom ` F ) e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` F ) ) /\ P e. NN0 /\ E e. ZZ ) -> ( ( ZRHom ` F ) ` ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) E ) ) = ( P .^ ( ( ZRHom ` F ) ` E ) ) )
51 46 11 12 50 syl3anc 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( ( ZRHom ` F ) ` ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) E ) ) = ( P .^ ( ( ZRHom ` F ) ` E ) ) )
52 6 10 zexpcld 
 |-  ( ph -> ( E ^ P ) e. ZZ )
53 eqid 
 |-  ( -g ` ZZring ) = ( -g ` ZZring )
54 53 zringsubgval 
 |-  ( ( ( E ^ P ) e. ZZ /\ E e. ZZ ) -> ( ( E ^ P ) - E ) = ( ( E ^ P ) ( -g ` ZZring ) E ) )
55 52 6 54 syl2anc 
 |-  ( ph -> ( ( E ^ P ) - E ) = ( ( E ^ P ) ( -g ` ZZring ) E ) )
56 55 fveq2d 
 |-  ( ph -> ( ( ZRHom ` F ) ` ( ( E ^ P ) - E ) ) = ( ( ZRHom ` F ) ` ( ( E ^ P ) ( -g ` ZZring ) E ) ) )
57 52 zred 
 |-  ( ph -> ( E ^ P ) e. RR )
58 6 zred 
 |-  ( ph -> E e. RR )
59 5 8 syl 
 |-  ( ph -> P e. NN )
60 59 nnrpd 
 |-  ( ph -> P e. RR+ )
61 fermltl 
 |-  ( ( P e. Prime /\ E e. ZZ ) -> ( ( E ^ P ) mod P ) = ( E mod P ) )
62 5 6 61 syl2anc 
 |-  ( ph -> ( ( E ^ P ) mod P ) = ( E mod P ) )
63 eqidd 
 |-  ( ph -> ( E mod P ) = ( E mod P ) )
64 57 58 58 58 60 62 63 modsub12d 
 |-  ( ph -> ( ( ( E ^ P ) - E ) mod P ) = ( ( E - E ) mod P ) )
65 zcn 
 |-  ( E e. ZZ -> E e. CC )
66 65 subidd 
 |-  ( E e. ZZ -> ( E - E ) = 0 )
67 6 66 syl 
 |-  ( ph -> ( E - E ) = 0 )
68 67 oveq1d 
 |-  ( ph -> ( ( E - E ) mod P ) = ( 0 mod P ) )
69 0mod 
 |-  ( P e. RR+ -> ( 0 mod P ) = 0 )
70 60 69 syl 
 |-  ( ph -> ( 0 mod P ) = 0 )
71 64 68 70 3eqtrd 
 |-  ( ph -> ( ( ( E ^ P ) - E ) mod P ) = 0 )
72 52 6 zsubcld 
 |-  ( ph -> ( ( E ^ P ) - E ) e. ZZ )
73 dvdsval3 
 |-  ( ( P e. NN /\ ( ( E ^ P ) - E ) e. ZZ ) -> ( P || ( ( E ^ P ) - E ) <-> ( ( ( E ^ P ) - E ) mod P ) = 0 ) )
74 59 72 73 syl2anc 
 |-  ( ph -> ( P || ( ( E ^ P ) - E ) <-> ( ( ( E ^ P ) - E ) mod P ) = 0 ) )
75 71 74 mpbird 
 |-  ( ph -> P || ( ( E ^ P ) - E ) )
76 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
77 1 39 76 chrdvds 
 |-  ( ( F e. Ring /\ ( ( E ^ P ) - E ) e. ZZ ) -> ( P || ( ( E ^ P ) - E ) <-> ( ( ZRHom ` F ) ` ( ( E ^ P ) - E ) ) = ( 0g ` F ) ) )
78 38 72 77 syl2anc 
 |-  ( ph -> ( P || ( ( E ^ P ) - E ) <-> ( ( ZRHom ` F ) ` ( ( E ^ P ) - E ) ) = ( 0g ` F ) ) )
79 75 78 mpbid 
 |-  ( ph -> ( ( ZRHom ` F ) ` ( ( E ^ P ) - E ) ) = ( 0g ` F ) )
80 rhmghm 
 |-  ( ( ZRHom ` F ) e. ( ZZring RingHom F ) -> ( ZRHom ` F ) e. ( ZZring GrpHom F ) )
81 41 80 syl 
 |-  ( ph -> ( ZRHom ` F ) e. ( ZZring GrpHom F ) )
82 zringbas 
 |-  ZZ = ( Base ` ZZring )
83 eqid 
 |-  ( -g ` F ) = ( -g ` F )
84 82 53 83 ghmsub 
 |-  ( ( ( ZRHom ` F ) e. ( ZZring GrpHom F ) /\ ( E ^ P ) e. ZZ /\ E e. ZZ ) -> ( ( ZRHom ` F ) ` ( ( E ^ P ) ( -g ` ZZring ) E ) ) = ( ( ( ZRHom ` F ) ` ( E ^ P ) ) ( -g ` F ) ( ( ZRHom ` F ) ` E ) ) )
85 81 52 6 84 syl3anc 
 |-  ( ph -> ( ( ZRHom ` F ) ` ( ( E ^ P ) ( -g ` ZZring ) E ) ) = ( ( ( ZRHom ` F ) ` ( E ^ P ) ) ( -g ` F ) ( ( ZRHom ` F ) ` E ) ) )
86 56 79 85 3eqtr3rd 
 |-  ( ph -> ( ( ( ZRHom ` F ) ` ( E ^ P ) ) ( -g ` F ) ( ( ZRHom ` F ) ` E ) ) = ( 0g ` F ) )
87 7 crnggrpd 
 |-  ( ph -> F e. Grp )
88 eqid 
 |-  ( Base ` F ) = ( Base ` F )
89 82 88 rhmf 
 |-  ( ( ZRHom ` F ) e. ( ZZring RingHom F ) -> ( ZRHom ` F ) : ZZ --> ( Base ` F ) )
90 41 89 syl 
 |-  ( ph -> ( ZRHom ` F ) : ZZ --> ( Base ` F ) )
91 90 52 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` F ) ` ( E ^ P ) ) e. ( Base ` F ) )
92 90 6 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` F ) ` E ) e. ( Base ` F ) )
93 88 76 83 grpsubeq0 
 |-  ( ( F e. Grp /\ ( ( ZRHom ` F ) ` ( E ^ P ) ) e. ( Base ` F ) /\ ( ( ZRHom ` F ) ` E ) e. ( Base ` F ) ) -> ( ( ( ( ZRHom ` F ) ` ( E ^ P ) ) ( -g ` F ) ( ( ZRHom ` F ) ` E ) ) = ( 0g ` F ) <-> ( ( ZRHom ` F ) ` ( E ^ P ) ) = ( ( ZRHom ` F ) ` E ) ) )
94 87 91 92 93 syl3anc 
 |-  ( ph -> ( ( ( ( ZRHom ` F ) ` ( E ^ P ) ) ( -g ` F ) ( ( ZRHom ` F ) ` E ) ) = ( 0g ` F ) <-> ( ( ZRHom ` F ) ` ( E ^ P ) ) = ( ( ZRHom ` F ) ` E ) ) )
95 86 94 mpbid 
 |-  ( ph -> ( ( ZRHom ` F ) ` ( E ^ P ) ) = ( ( ZRHom ` F ) ` E ) )
96 95 adantr 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( ( ZRHom ` F ) ` ( E ^ P ) ) = ( ( ZRHom ` F ) ` E ) )
97 37 51 96 3eqtr3d 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( P .^ ( ( ZRHom ` F ) ` E ) ) = ( ( ZRHom ` F ) ` E ) )
98 oveq2 
 |-  ( A = ( ( ZRHom ` F ) ` E ) -> ( P .^ A ) = ( P .^ ( ( ZRHom ` F ) ` E ) ) )
99 98 adantl 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( P .^ A ) = ( P .^ ( ( ZRHom ` F ) ` E ) ) )
100 simpr 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> A = ( ( ZRHom ` F ) ` E ) )
101 97 99 100 3eqtr4d 
 |-  ( ( ph /\ A = ( ( ZRHom ` F ) ` E ) ) -> ( P .^ A ) = A )
102 4 101 mpan2 
 |-  ( ph -> ( P .^ A ) = A )