Definition df-finfld 46234

Description: Define a function taking a prime power 𝑞 to the finite field of order 𝑞. When 𝑞 is an integer, there is a field of order 𝑞 (that is, its base set has 𝑞 elements) if and only if 𝑞 is a prime power. Additionally, any two finite fields of the same order are isomorphic. Thus, we usually refer to "the" finite field of order 𝑞 — which is often denoted 𝔽 _𝑞 — without specifying a particular one. Usually, this causes no problems, but in Metamath the notation (𝔽‘𝑞) must unambigously denote a specific set. Since HFStructs can be well-ordered, we can use the smallest candidate according to the ordering. This depends on the fact that any finite field is isomorphic to an HFStruct. Indeed, this isomorphism result holds for most abstract mathematical structures with a finite base set. (For groups, see fingrphf 46229.) Thus, the technique used here could apply in other cases in which we want a particular representative of some class of finite structures. (Contributed by Eric Schmidt, 24-Oct-2026.)

Assertion

Ref	Expression
df-finfld	⊢ 𝔽 = (𝑞 ∈ (↑ “ (ℙ × ℕ)) ↦ inf((HFStruct ∩ {𝑘 ∈ Field ∣ (♯‘(Base‘𝑘)) = 𝑞}), HFStruct, <HFStruct ))

Distinct variable group:   𝑘,𝑞

Detailed syntax breakdown of Definition df-finfld

Step	Hyp	Ref	Expression
1		cfinfld 46233	. 2 class 𝔽
2		vq	. . 3 setvar 𝑞
3		cexp 14228	. . . 4 class ↑
4		cprime 16872	. . . . 5 class ℙ
5		cn 12359	. . . . 5 class ℕ
6	4, 5	cxp 5653	. . . 4 class (ℙ × ℕ)
7	3, 6	cima 5658	. . 3 class (↑ “ (ℙ × ℕ))
8		chfstruct 46219	. . . . 5 class HFStruct
9		vk	. . . . . . . . . 10 setvar 𝑘
10	9	cv 1569	. . . . . . . . 9 class 𝑘
11		cbs 17413	. . . . . . . . 9 class Base
12	10, 11	cfv 6555	. . . . . . . 8 class (Base‘𝑘)
13		chash 14498	. . . . . . . 8 class ♯
14	12, 13	cfv 6555	. . . . . . 7 class (♯‘(Base‘𝑘))
15	2	cv 1569	. . . . . . 7 class 𝑞
16	14, 15	wceq 1570	. . . . . 6 wff (♯‘(Base‘𝑘)) = 𝑞
17		cfield 21008	. . . . . 6 class Field
18	16, 9, 17	crab 3416	. . . . 5 class {𝑘 ∈ Field ∣ (♯‘(Base‘𝑘)) = 𝑞}
19	8, 18	cin 4092	. . . 4 class (HFStruct ∩ {𝑘 ∈ Field ∣ (♯‘(Base‘𝑘)) = 𝑞})
20		clthfstruct 46230	. . . 4 class <HFStruct
21	19, 8, 20	cinf 9457	. . 3 class inf((HFStruct ∩ {𝑘 ∈ Field ∣ (♯‘(Base‘𝑘)) = 𝑞}), HFStruct, <HFStruct )
22	2, 7, 21	cmpt 5189	. 2 class (𝑞 ∈ (↑ “ (ℙ × ℕ)) ↦ inf((HFStruct ∩ {𝑘 ∈ Field ∣ (♯‘(Base‘𝑘)) = 𝑞}), HFStruct, <HFStruct ))
23	1, 22	wceq 1570	1 wff 𝔽 = (𝑞 ∈ (↑ “ (ℙ × ℕ)) ↦ inf((HFStruct ∩ {𝑘 ∈ Field ∣ (♯‘(Base‘𝑘)) = 𝑞}), HFStruct, <HFStruct ))

This definition is used by: (None)