Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gf Structured version   Visualization version   GIF version

Definition df-gf 32957
 Description: Define the Galois finite field of order 𝑝↑𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-gf GF = (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑝) / 𝑟(1st ‘(𝑟 splitFld {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)})))
Distinct variable group:   𝑛,𝑝,𝑟,𝑠,𝑥

Detailed syntax breakdown of Definition df-gf
StepHypRef Expression
1 cgf 32948 . 2 class GF
2 vp . . 3 setvar 𝑝
3 vn . . 3 setvar 𝑛
4 cprime 16013 . . 3 class
5 cn 11634 . . 3 class
6 vr . . . 4 setvar 𝑟
72cv 1537 . . . . 5 class 𝑝
8 czn 20650 . . . . 5 class ℤ/n
97, 8cfv 6343 . . . 4 class (ℤ/nℤ‘𝑝)
106cv 1537 . . . . . 6 class 𝑟
11 vs . . . . . . . 8 setvar 𝑠
12 cpl1 20345 . . . . . . . . 9 class Poly1
1310, 12cfv 6343 . . . . . . . 8 class (Poly1𝑟)
14 vx . . . . . . . . 9 setvar 𝑥
15 cv1 20344 . . . . . . . . . 10 class var1
1610, 15cfv 6343 . . . . . . . . 9 class (var1𝑟)
173cv 1537 . . . . . . . . . . . 12 class 𝑛
18 cexp 13434 . . . . . . . . . . . 12 class
197, 17, 18co 7149 . . . . . . . . . . 11 class (𝑝𝑛)
2014cv 1537 . . . . . . . . . . 11 class 𝑥
2111cv 1537 . . . . . . . . . . . . 13 class 𝑠
22 cmgp 19239 . . . . . . . . . . . . 13 class mulGrp
2321, 22cfv 6343 . . . . . . . . . . . 12 class (mulGrp‘𝑠)
24 cmg 18224 . . . . . . . . . . . 12 class .g
2523, 24cfv 6343 . . . . . . . . . . 11 class (.g‘(mulGrp‘𝑠))
2619, 20, 25co 7149 . . . . . . . . . 10 class ((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)
27 csg 18105 . . . . . . . . . . 11 class -g
2821, 27cfv 6343 . . . . . . . . . 10 class (-g𝑠)
2926, 20, 28co 7149 . . . . . . . . 9 class (((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)
3014, 16, 29csb 3866 . . . . . . . 8 class (var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)
3111, 13, 30csb 3866 . . . . . . 7 class (Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)
3231csn 4550 . . . . . 6 class {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)}
33 csf 32937 . . . . . 6 class splitFld
3410, 32, 33co 7149 . . . . 5 class (𝑟 splitFld {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)})
35 c1st 7682 . . . . 5 class 1st
3634, 35cfv 6343 . . . 4 class (1st ‘(𝑟 splitFld {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)}))
376, 9, 36csb 3866 . . 3 class (ℤ/nℤ‘𝑝) / 𝑟(1st ‘(𝑟 splitFld {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)}))
382, 3, 4, 5, 37cmpo 7151 . 2 class (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑝) / 𝑟(1st ‘(𝑟 splitFld {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)})))
391, 38wceq 1538 1 wff GF = (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ (ℤ/nℤ‘𝑝) / 𝑟(1st ‘(𝑟 splitFld {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)})))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator