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

Definition df-gfoo 30804
Description: Define the Galois field of order 𝑝↑+∞, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-gfoo GF = (𝑝 ∈ ℙ ↦ (ℤ/nℤ‘𝑝) / 𝑟(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)})))
Distinct variable group:   𝑛,𝑝,𝑟,𝑠,𝑥

Detailed syntax breakdown of Definition df-gfoo
StepHypRef Expression
1 cgfo 30794 . 2 class GF
2 vp . . 3 setvar 𝑝
3 cprime 15223 . . 3 class
4 vr . . . 4 setvar 𝑟
52cv 1474 . . . . 5 class 𝑝
6 czn 19670 . . . . 5 class ℤ/n
75, 6cfv 5804 . . . 4 class (ℤ/nℤ‘𝑝)
84cv 1474 . . . . 5 class 𝑟
9 vn . . . . . 6 setvar 𝑛
10 cn 10897 . . . . . 6 class
11 vs . . . . . . . 8 setvar 𝑠
12 cpl1 19368 . . . . . . . . 9 class Poly1
138, 12cfv 5804 . . . . . . . 8 class (Poly1𝑟)
14 vx . . . . . . . . 9 setvar 𝑥
15 cv1 19367 . . . . . . . . . 10 class var1
168, 15cfv 5804 . . . . . . . . 9 class (var1𝑟)
179cv 1474 . . . . . . . . . . . 12 class 𝑛
18 cexp 12722 . . . . . . . . . . . 12 class
195, 17, 18co 6549 . . . . . . . . . . 11 class (𝑝𝑛)
2014cv 1474 . . . . . . . . . . 11 class 𝑥
2111cv 1474 . . . . . . . . . . . . 13 class 𝑠
22 cmgp 18312 . . . . . . . . . . . . 13 class mulGrp
2321, 22cfv 5804 . . . . . . . . . . . 12 class (mulGrp‘𝑠)
24 cmg 17363 . . . . . . . . . . . 12 class .g
2523, 24cfv 5804 . . . . . . . . . . 11 class (.g‘(mulGrp‘𝑠))
2619, 20, 25co 6549 . . . . . . . . . 10 class ((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)
27 csg 17247 . . . . . . . . . . 11 class -g
2821, 27cfv 5804 . . . . . . . . . 10 class (-g𝑠)
2926, 20, 28co 6549 . . . . . . . . 9 class (((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)
3014, 16, 29csb 3499 . . . . . . . 8 class (var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)
3111, 13, 30csb 3499 . . . . . . 7 class (Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)
3231csn 4125 . . . . . 6 class {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)}
339, 10, 32cmpt 4643 . . . . 5 class (𝑛 ∈ ℕ ↦ {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)})
34 cpsl 30783 . . . . 5 class polySplitLim
358, 33, 34co 6549 . . . 4 class (𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)}))
364, 7, 35csb 3499 . . 3 class (ℤ/nℤ‘𝑝) / 𝑟(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)}))
372, 3, 36cmpt 4643 . 2 class (𝑝 ∈ ℙ ↦ (ℤ/nℤ‘𝑝) / 𝑟(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)})))
381, 37wceq 1475 1 wff GF = (𝑝 ∈ ℙ ↦ (ℤ/nℤ‘𝑝) / 𝑟(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {(Poly1𝑟) / 𝑠(var1𝑟) / 𝑥(((𝑝𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g𝑠)𝑥)})))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator