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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
frobrhm.2 ⊢ 𝑃 = ( chr ‘ 𝑅 )
frobrhm.3 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
frobrhm.4 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑃 ↑ 𝑥 ) )
frobrhm.5 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
frobrhm.6 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
Assertion frobrhm ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑅 ) )

Proof

Step Hyp Ref Expression
1 frobrhm.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 frobrhm.2 ⊢ 𝑃 = ( chr ‘ 𝑅 )
3 frobrhm.3 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
4 frobrhm.4 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑃 ↑ 𝑥 ) )
5 frobrhm.5 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 frobrhm.6 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9 5 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = ( 1r ‘ 𝑅 ) ) → 𝑥 = ( 1r ‘ 𝑅 ) )
11 10 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = ( 1r ‘ 𝑅 ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( 1r ‘ 𝑅 ) ) )
12 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
13 12 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
14 9 13 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
15 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
16 nnnn0 ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
17 6 15 16 3syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
18 12 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
19 12 7 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
20 18 3 19 mulgnn0z ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑃 ∈ ℕ0 ) → ( 𝑃 ↑ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
21 14 17 20 syl2anc ⊢ ( 𝜑 → ( 𝑃 ↑ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = ( 1r ‘ 𝑅 ) ) → ( 𝑃 ↑ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
23 11 22 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = ( 1r ‘ 𝑅 ) ) → ( 𝑃 ↑ 𝑥 ) = ( 1r ‘ 𝑅 ) )
24 1 7 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
25 9 24 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
26 4 23 25 25 fvmptd2 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
27 12 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
28 5 27 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
30 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑃 ∈ ℕ0 )
31 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑖 ∈ 𝐵 )
32 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑗 ∈ 𝐵 )
33 12 8 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
34 18 3 33 mulgnn0di ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ∧ ( 𝑃 ∈ ℕ0 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) = ( ( 𝑃 ↑ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑃 ↑ 𝑗 ) ) )
35 29 30 31 32 34 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) = ( ( 𝑃 ↑ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑃 ↑ 𝑗 ) ) )
36 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) → 𝑥 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) )
37 36 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) )
38 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
39 1 8 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) → ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ∈ 𝐵 )
40 38 31 32 39 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ∈ 𝐵 )
41 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) ∈ V )
42 4 37 40 41 fvmptd2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) = ( 𝑃 ↑ ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) )
43 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = 𝑖 ) → 𝑥 = 𝑖 )
44 43 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = 𝑖 ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ 𝑖 ) )
45 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ 𝑖 ) ∈ V )
46 4 44 31 45 fvmptd2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ↑ 𝑖 ) )
47 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = 𝑗 ) → 𝑥 = 𝑗 )
48 47 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = 𝑗 ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ 𝑗 ) )
49 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ 𝑗 ) ∈ V )
50 4 48 32 49 fvmptd2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝑃 ↑ 𝑗 ) )
51 46 50 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝑃 ↑ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑃 ↑ 𝑗 ) ) )
52 35 42 51 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑖 ( .r ‘ 𝑅 ) 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) )
53 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
54 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
55 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑃 ∈ ℕ0 )
56 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
57 18 3 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑃 ∈ ℕ0 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑃 ↑ 𝑥 ) ∈ 𝐵 )
58 54 55 56 57 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑃 ↑ 𝑥 ) ∈ 𝐵 )
59 58 4 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐵 )
60 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑅 ∈ CRing )
61 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑃 ∈ ℙ )
62 1 53 3 2 60 61 31 32 freshmansdream ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) = ( ( 𝑃 ↑ 𝑖 ) ( +g ‘ 𝑅 ) ( 𝑃 ↑ 𝑗 ) ) )
63 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) → 𝑥 = ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) )
64 63 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) )
65 1 53 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ∈ 𝐵 )
66 38 31 32 65 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ∈ 𝐵 )
67 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) ∈ V )
68 4 64 66 67 fvmptd2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) = ( 𝑃 ↑ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) )
69 46 50 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑖 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝑃 ↑ 𝑖 ) ( +g ‘ 𝑅 ) ( 𝑃 ↑ 𝑗 ) ) )
70 62 68 69 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) )
71 1 7 7 8 8 9 9 26 52 1 53 53 59 70 isrhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑅 ) )