Metamath Proof Explorer

Theorem frobrhm

Description: In a commutative ring with prime characteristic, the Frobenius function F is a ring endomorphism, thus named the Frobenius endomorphism. (Contributed by Thierry Arnoux, 31-May-2024)

Ref Expression
Hypotheses frobrhm.1 
|- B = ( Base ` R )
frobrhm.2 
|- P = ( chr ` R )
frobrhm.3 
|- .^ = ( .g ` ( mulGrp ` R ) )
frobrhm.4 
|- F = ( x e. B |-> ( P .^ x ) )
frobrhm.5 
|- ( ph -> R e. CRing )
frobrhm.6 
|- ( ph -> P e. Prime )
Assertion frobrhm 
|- ( ph -> F e. ( R RingHom R ) )

Proof

Step Hyp Ref Expression
1 frobrhm.1 
 |-  B = ( Base ` R )
2 frobrhm.2 
 |-  P = ( chr ` R )
3 frobrhm.3 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
4 frobrhm.4 
 |-  F = ( x e. B |-> ( P .^ x ) )
5 frobrhm.5 
 |-  ( ph -> R e. CRing )
6 frobrhm.6 
 |-  ( ph -> P e. Prime )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 5 crngringd 
 |-  ( ph -> R e. Ring )
10 simpr 
 |-  ( ( ph /\ x = ( 1r ` R ) ) -> x = ( 1r ` R ) )
11 10 oveq2d 
 |-  ( ( ph /\ x = ( 1r ` R ) ) -> ( P .^ x ) = ( P .^ ( 1r ` R ) ) )
12 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
13 12 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
14 9 13 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
15 prmnn 
 |-  ( P e. Prime -> P e. NN )
16 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
17 6 15 16 3syl 
 |-  ( ph -> P e. NN0 )
18 12 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
19 12 7 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
20 18 3 19 mulgnn0z 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ P e. NN0 ) -> ( P .^ ( 1r ` R ) ) = ( 1r ` R ) )
21 14 17 20 syl2anc 
 |-  ( ph -> ( P .^ ( 1r ` R ) ) = ( 1r ` R ) )
22 21 adantr 
 |-  ( ( ph /\ x = ( 1r ` R ) ) -> ( P .^ ( 1r ` R ) ) = ( 1r ` R ) )
23 11 22 eqtrd 
 |-  ( ( ph /\ x = ( 1r ` R ) ) -> ( P .^ x ) = ( 1r ` R ) )
24 1 7 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
25 9 24 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
26 4 23 25 25 fvmptd2 
 |-  ( ph -> ( F ` ( 1r ` R ) ) = ( 1r ` R ) )
27 12 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
28 5 27 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
29 28 adantr 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( mulGrp ` R ) e. CMnd )
30 17 adantr 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> P e. NN0 )
31 simprl 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> i e. B )
32 simprr 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> j e. B )
33 12 8 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
34 18 3 33 mulgnn0di 
 |-  ( ( ( mulGrp ` R ) e. CMnd /\ ( P e. NN0 /\ i e. B /\ j e. B ) ) -> ( P .^ ( i ( .r ` R ) j ) ) = ( ( P .^ i ) ( .r ` R ) ( P .^ j ) ) )
35 29 30 31 32 34 syl13anc 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( P .^ ( i ( .r ` R ) j ) ) = ( ( P .^ i ) ( .r ` R ) ( P .^ j ) ) )
36 simpr 
 |-  ( ( ( ph /\ ( i e. B /\ j e. B ) ) /\ x = ( i ( .r ` R ) j ) ) -> x = ( i ( .r ` R ) j ) )
37 36 oveq2d 
 |-  ( ( ( ph /\ ( i e. B /\ j e. B ) ) /\ x = ( i ( .r ` R ) j ) ) -> ( P .^ x ) = ( P .^ ( i ( .r ` R ) j ) ) )
38 9 adantr 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> R e. Ring )
39 1 8 ringcl 
 |-  ( ( R e. Ring /\ i e. B /\ j e. B ) -> ( i ( .r ` R ) j ) e. B )
40 38 31 32 39 syl3anc 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( i ( .r ` R ) j ) e. B )
41 ovexd 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( P .^ ( i ( .r ` R ) j ) ) e. _V )
42 4 37 40 41 fvmptd2 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( F ` ( i ( .r ` R ) j ) ) = ( P .^ ( i ( .r ` R ) j ) ) )
43 simpr 
 |-  ( ( ( ph /\ ( i e. B /\ j e. B ) ) /\ x = i ) -> x = i )
44 43 oveq2d 
 |-  ( ( ( ph /\ ( i e. B /\ j e. B ) ) /\ x = i ) -> ( P .^ x ) = ( P .^ i ) )
45 ovexd 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( P .^ i ) e. _V )
46 4 44 31 45 fvmptd2 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( F ` i ) = ( P .^ i ) )
47 simpr 
 |-  ( ( ( ph /\ ( i e. B /\ j e. B ) ) /\ x = j ) -> x = j )
48 47 oveq2d 
 |-  ( ( ( ph /\ ( i e. B /\ j e. B ) ) /\ x = j ) -> ( P .^ x ) = ( P .^ j ) )
49 ovexd 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( P .^ j ) e. _V )
50 4 48 32 49 fvmptd2 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( F ` j ) = ( P .^ j ) )
51 46 50 oveq12d 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( ( F ` i ) ( .r ` R ) ( F ` j ) ) = ( ( P .^ i ) ( .r ` R ) ( P .^ j ) ) )
52 35 42 51 3eqtr4d 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( F ` ( i ( .r ` R ) j ) ) = ( ( F ` i ) ( .r ` R ) ( F ` j ) ) )
53 eqid 
 |-  ( +g ` R ) = ( +g ` R )
54 14 adantr 
 |-  ( ( ph /\ x e. B ) -> ( mulGrp ` R ) e. Mnd )
55 17 adantr 
 |-  ( ( ph /\ x e. B ) -> P e. NN0 )
56 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
57 18 3 54 55 56 mulgnn0cld 
 |-  ( ( ph /\ x e. B ) -> ( P .^ x ) e. B )
58 57 4 fmptd 
 |-  ( ph -> F : B --> B )
59 5 adantr 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> R e. CRing )
60 6 adantr 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> P e. Prime )
61 1 53 3 2 59 60 31 32 freshmansdream 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( P .^ ( i ( +g ` R ) j ) ) = ( ( P .^ i ) ( +g ` R ) ( P .^ j ) ) )
62 simpr 
 |-  ( ( ( ph /\ ( i e. B /\ j e. B ) ) /\ x = ( i ( +g ` R ) j ) ) -> x = ( i ( +g ` R ) j ) )
63 62 oveq2d 
 |-  ( ( ( ph /\ ( i e. B /\ j e. B ) ) /\ x = ( i ( +g ` R ) j ) ) -> ( P .^ x ) = ( P .^ ( i ( +g ` R ) j ) ) )
64 1 53 ringacl 
 |-  ( ( R e. Ring /\ i e. B /\ j e. B ) -> ( i ( +g ` R ) j ) e. B )
65 38 31 32 64 syl3anc 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( i ( +g ` R ) j ) e. B )
66 ovexd 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( P .^ ( i ( +g ` R ) j ) ) e. _V )
67 4 63 65 66 fvmptd2 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( F ` ( i ( +g ` R ) j ) ) = ( P .^ ( i ( +g ` R ) j ) ) )
68 46 50 oveq12d 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( ( F ` i ) ( +g ` R ) ( F ` j ) ) = ( ( P .^ i ) ( +g ` R ) ( P .^ j ) ) )
69 61 67 68 3eqtr4d 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( F ` ( i ( +g ` R ) j ) ) = ( ( F ` i ) ( +g ` R ) ( F ` j ) ) )
70 1 7 7 8 8 9 9 26 52 1 53 53 58 69 isrhmd 
 |-  ( ph -> F e. ( R RingHom R ) )