Definition df-gf 31549

Description: Define the Galois finite field of order p ^ n. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

Ref	Expression
df-gf	|- GF = ( p e. Prime , n e. NN |-> [_ (ℤ/nℤ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )

Distinct variable group:   n, p, r, s, x

Detailed syntax breakdown of Definition df-gf

Step	Hyp	Ref	Expression
1		cgf 31539	. 2 class GF
2		vp	. . 3 setvar p
3		vn	. . 3 setvar n
4		cprime 15385	. . 3 class Prime
5		cn 11020	. . 3 class NN
6		vr	. . . 4 setvar r
7	2	cv 1482	. . . . 5 class p
8		czn 19851	. . . . 5 class ℤ/nℤ
9	7, 8	cfv 5888	. . . 4 class (ℤ/nℤ ` p )
10	6	cv 1482	. . . . . 6 class r
11		vs	. . . . . . . 8 setvar s
12		cpl1 19547	. . . . . . . . 9 class Poly1
13	10, 12	cfv 5888	. . . . . . . 8 class (Poly1 ` r )
14		vx	. . . . . . . . 9 setvar x
15		cv1 19546	. . . . . . . . . 10 class var1
16	10, 15	cfv 5888	. . . . . . . . 9 class (var1 ` r )
17	3	cv 1482	. . . . . . . . . . . 12 class n
18		cexp 12860	. . . . . . . . . . . 12 class ^
19	7, 17, 18	co 6650	. . . . . . . . . . 11 class ( p ^ n )
20	14	cv 1482	. . . . . . . . . . 11 class x
21	11	cv 1482	. . . . . . . . . . . . 13 class s
22		cmgp 18489	. . . . . . . . . . . . 13 class mulGrp
23	21, 22	cfv 5888	. . . . . . . . . . . 12 class (mulGrp ` s )
24		cmg 17540	. . . . . . . . . . . 12 class .g
25	23, 24	cfv 5888	. . . . . . . . . . 11 class (.g ` (mulGrp ` s ) )
26	19, 20, 25	co 6650	. . . . . . . . . 10 class ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x )
27		csg 17424	. . . . . . . . . . 11 class -g
28	21, 27	cfv 5888	. . . . . . . . . 10 class ( -g ` s )
29	26, 20, 28	co 6650	. . . . . . . . 9 class ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x )
30	14, 16, 29	csb 3533	. . . . . . . 8 class [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x )
31	11, 13, 30	csb 3533	. . . . . . 7 class [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x )
32	31	csn 4177	. . . . . 6 class { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) }
33		csf 31528	. . . . . 6 class splitFld
34	10, 32, 33	co 6650	. . . . 5 class ( r splitFld { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } )
35		c1st 7166	. . . . 5 class 1st
36	34, 35	cfv 5888	. . . 4 class ( 1st ` ( r splitFld { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) )
37	6, 9, 36	csb 3533	. . 3 class [_ (ℤ/nℤ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) )
38	2, 3, 4, 5, 37	cmpt2 6652	. 2 class ( p e. Prime , n e. NN |-> [_ (ℤ/nℤ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )
39	1, 38	wceq 1483	1 wff GF = ( p e. Prime , n e. NN |-> [_ (ℤ/nℤ ` p ) / r ]_ ( 1st ` ( r splitFld { [_ (Poly1 ` r ) / s ]_ [_ (var1 ` r ) / x ]_ ( ( ( p ^ n ) (.g ` (mulGrp ` s ) ) x ) ( -g ` s ) x ) } ) ) )

This definition is referenced by: (None)