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	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
	frobrhm.4	$⊢ F = (x \in B ⟼ P \underset{˙}{\times} x)$
	frobrhm.5	$⊢ φ \to R \in CRing$
	frobrhm.6	$⊢ φ \to P \in ℙ$
Assertion	frobrhm	$⊢ φ \to F \in (R RingHom R)$

Proof

Step	Hyp	Ref	Expression
1		frobrhm.1	$⊢ B = {Base}_{R}$
2		frobrhm.2	$⊢ P = chr (R)$
3		frobrhm.3	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
4		frobrhm.4	$⊢ F = (x \in B ⟼ P \underset{˙}{\times} x)$
5		frobrhm.5	$⊢ φ \to R \in CRing$
6		frobrhm.6	$⊢ φ \to P \in ℙ$
7		eqid	$⊢ 1_{R} = 1_{R}$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9	5	crngringd	$⊢ φ \to R \in Ring$
10		simpr	$⊢ (φ \land x = 1_{R}) \to x = 1_{R}$
11	10	oveq2d	$⊢ (φ \land x = 1_{R}) \to P \underset{˙}{\times} x = P \underset{˙}{\times} 1_{R}$
12		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
13	12	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
14	9 13	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
15		prmnn	$⊢ P \in ℙ \to P \in ℕ$
16		nnnn0	$⊢ P \in ℕ \to P \in ℕ_{0}$
17	6 15 16	3syl	$⊢ φ \to P \in ℕ_{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} \in Mnd \land P \in ℕ_{0}) \to P \underset{˙}{\times} 1_{R} = 1_{R}$
21	14 17 20	syl2anc	$⊢ φ \to P \underset{˙}{\times} 1_{R} = 1_{R}$
22	21	adantr	$⊢ (φ \land x = 1_{R}) \to P \underset{˙}{\times} 1_{R} = 1_{R}$
23	11 22	eqtrd	$⊢ (φ \land x = 1_{R}) \to P \underset{˙}{\times} x = 1_{R}$
24	1 7	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
25	9 24	syl	$⊢ φ \to 1_{R} \in B$
26	4 23 25 25	fvmptd2	$⊢ φ \to F (1_{R}) = 1_{R}$
27	12	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
28	5 27	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
29	28	adantr	$⊢ (φ \land (i \in B \land j \in B)) \to {mulGrp}_{R} \in CMnd$
30	17	adantr	$⊢ (φ \land (i \in B \land j \in B)) \to P \in ℕ_{0}$
31		simprl	$⊢ (φ \land (i \in B \land j \in B)) \to i \in B$
32		simprr	$⊢ (φ \land (i \in B \land j \in B)) \to j \in B$
33	12 8	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
34	18 3 33	mulgnn0di	$⊢ ({mulGrp}_{R} \in CMnd \land (P \in ℕ_{0} \land i \in B \land j \in B)) \to P \underset{˙}{\times} (i \cdot_{R} j) = (P \underset{˙}{\times} i) \cdot_{R} (P \underset{˙}{\times} j)$
35	29 30 31 32 34	syl13anc	$⊢ (φ \land (i \in B \land j \in B)) \to P \underset{˙}{\times} (i \cdot_{R} j) = (P \underset{˙}{\times} i) \cdot_{R} (P \underset{˙}{\times} j)$
36		simpr	$⊢ ((φ \land (i \in B \land j \in B)) \land x = i \cdot_{R} j) \to x = i \cdot_{R} j$
37	36	oveq2d	$⊢ ((φ \land (i \in B \land j \in B)) \land x = i \cdot_{R} j) \to P \underset{˙}{\times} x = P \underset{˙}{\times} (i \cdot_{R} j)$
38	9	adantr	$⊢ (φ \land (i \in B \land j \in B)) \to R \in Ring$
39	1 8	ringcl	$⊢ (R \in Ring \land i \in B \land j \in B) \to i \cdot_{R} j \in B$
40	38 31 32 39	syl3anc	$⊢ (φ \land (i \in B \land j \in B)) \to i \cdot_{R} j \in B$
41		ovexd	$⊢ (φ \land (i \in B \land j \in B)) \to P \underset{˙}{\times} (i \cdot_{R} j) \in V$
42	4 37 40 41	fvmptd2	$⊢ (φ \land (i \in B \land j \in B)) \to F (i \cdot_{R} j) = P \underset{˙}{\times} (i \cdot_{R} j)$
43		simpr	$⊢ ((φ \land (i \in B \land j \in B)) \land x = i) \to x = i$
44	43	oveq2d	$⊢ ((φ \land (i \in B \land j \in B)) \land x = i) \to P \underset{˙}{\times} x = P \underset{˙}{\times} i$
45		ovexd	$⊢ (φ \land (i \in B \land j \in B)) \to P \underset{˙}{\times} i \in V$
46	4 44 31 45	fvmptd2	$⊢ (φ \land (i \in B \land j \in B)) \to F (i) = P \underset{˙}{\times} i$
47		simpr	$⊢ ((φ \land (i \in B \land j \in B)) \land x = j) \to x = j$
48	47	oveq2d	$⊢ ((φ \land (i \in B \land j \in B)) \land x = j) \to P \underset{˙}{\times} x = P \underset{˙}{\times} j$
49		ovexd	$⊢ (φ \land (i \in B \land j \in B)) \to P \underset{˙}{\times} j \in V$
50	4 48 32 49	fvmptd2	$⊢ (φ \land (i \in B \land j \in B)) \to F (j) = P \underset{˙}{\times} j$
51	46 50	oveq12d	$⊢ (φ \land (i \in B \land j \in B)) \to F (i) \cdot_{R} F (j) = (P \underset{˙}{\times} i) \cdot_{R} (P \underset{˙}{\times} j)$
52	35 42 51	3eqtr4d	$⊢ (φ \land (i \in B \land j \in B)) \to F (i \cdot_{R} j) = F (i) \cdot_{R} F (j)$
53		eqid	$⊢ +_{R} = +_{R}$
54	14	adantr	$⊢ (φ \land x \in B) \to {mulGrp}_{R} \in Mnd$
55	17	adantr	$⊢ (φ \land x \in B) \to P \in ℕ_{0}$
56		simpr	$⊢ (φ \land x \in B) \to x \in B$
57	18 3	mulgnn0cl	$⊢ ({mulGrp}_{R} \in Mnd \land P \in ℕ_{0} \land x \in B) \to P \underset{˙}{\times} x \in B$
58	54 55 56 57	syl3anc	$⊢ (φ \land x \in B) \to P \underset{˙}{\times} x \in B$
59	58 4	fmptd	$⊢ φ \to F : B ⟶ B$
60	5	adantr	$⊢ (φ \land (i \in B \land j \in B)) \to R \in CRing$
61	6	adantr	$⊢ (φ \land (i \in B \land j \in B)) \to P \in ℙ$
62	1 53 3 2 60 61 31 32	freshmansdream	$⊢ (φ \land (i \in B \land j \in B)) \to P \underset{˙}{\times} (i +_{R} j) = (P \underset{˙}{\times} i) +_{R} (P \underset{˙}{\times} j)$
63		simpr	$⊢ ((φ \land (i \in B \land j \in B)) \land x = i +_{R} j) \to x = i +_{R} j$
64	63	oveq2d	$⊢ ((φ \land (i \in B \land j \in B)) \land x = i +_{R} j) \to P \underset{˙}{\times} x = P \underset{˙}{\times} (i +_{R} j)$
65	1 53	ringacl	$⊢ (R \in Ring \land i \in B \land j \in B) \to i +_{R} j \in B$
66	38 31 32 65	syl3anc	$⊢ (φ \land (i \in B \land j \in B)) \to i +_{R} j \in B$
67		ovexd	$⊢ (φ \land (i \in B \land j \in B)) \to P \underset{˙}{\times} (i +_{R} j) \in V$
68	4 64 66 67	fvmptd2	$⊢ (φ \land (i \in B \land j \in B)) \to F (i +_{R} j) = P \underset{˙}{\times} (i +_{R} j)$
69	46 50	oveq12d	$⊢ (φ \land (i \in B \land j \in B)) \to F (i) +_{R} F (j) = (P \underset{˙}{\times} i) +_{R} (P \underset{˙}{\times} j)$
70	62 68 69	3eqtr4d	$⊢ (φ \land (i \in B \land j \in B)) \to 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	$⊢ φ \to F \in (R RingHom R)$

Metamath Proof Explorer

Theorem frobrhm

Proof