This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 54 55 56 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑃 ↑ 𝑥 ) ∈ 𝐵 )
58 57 4 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐵 )
59 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑅 ∈ CRing )
60 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑃 ∈ ℙ )
61 1 53 3 2 59 60 31 32 freshmansdream ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) = ( ( 𝑃 ↑ 𝑖 ) ( +g ‘ 𝑅 ) ( 𝑃 ↑ 𝑗 ) ) )
62 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) → 𝑥 = ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) )
63 62 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) )
64 1 53 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ∈ 𝐵 )
65 38 31 32 64 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ∈ 𝐵 )
66 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑃 ↑ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) ∈ V )
67 4 63 65 66 fvmptd2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) = ( 𝑃 ↑ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) )
68 46 50 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑖 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝑃 ↑ 𝑖 ) ( +g ‘ 𝑅 ) ( 𝑃 ↑ 𝑗 ) ) )
69 61 67 68 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑖 ( +g ‘ 𝑅 ) 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) )
70 1 7 7 8 8 9 9 26 52 1 53 53 58 69 isrhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑅 ) )