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 × ˙ = mulGrp R
frobrhm.4 F = x B P × ˙ x
frobrhm.5 φ R CRing
frobrhm.6 φ P
Assertion frobrhm φ F R RingHom R

Proof

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