Definition df-plfl 31534

Description: Define the field extension that augments a field with the root of the given irreducible polynomial, and extends the norm if one exists and the extension is unique. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

Ref

Expression

df-plfl

|- polyFld = ( r e. _V , p e. _V |-> [_ (Poly1 ` r ) / s ]_ [_ ( (RSpan ` s ) ` { p } ) / i ]_ [_ ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_ <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >. )

Distinct variable group:   f, g, i, n, p, q, r, s, t, z

Detailed syntax breakdown of Definition df-plfl

Step	Hyp	Ref	Expression
1		cpfl 31526	. 2 class polyFld
2		vr	. . 3 setvar r
3		vp	. . 3 setvar p
4		cvv 3200	. . 3 class _V
5		vs	. . . 4 setvar s
6	2	cv 1482	. . . . 5 class r
7		cpl1 19547	. . . . 5 class Poly1
8	6, 7	cfv 5888	. . . 4 class (Poly1 ` r )
9		vi	. . . . 5 setvar i
10	3	cv 1482	. . . . . . 7 class p
11	10	csn 4177	. . . . . 6 class { p }
12	5	cv 1482	. . . . . . 7 class s
13		crsp 19171	. . . . . . 7 class RSpan
14	12, 13	cfv 5888	. . . . . 6 class (RSpan ` s )
15	11, 14	cfv 5888	. . . . 5 class ( (RSpan ` s ) ` { p } )
16		vf	. . . . . 6 setvar f
17		vz	. . . . . . 7 setvar z
18		cbs 15857	. . . . . . . 8 class Base
19	6, 18	cfv 5888	. . . . . . 7 class ( Base ` r )
20	17	cv 1482	. . . . . . . . 9 class z
21		cur 18501	. . . . . . . . . 10 class 1r
22	12, 21	cfv 5888	. . . . . . . . 9 class ( 1r ` s )
23		cvsca 15945	. . . . . . . . . 10 class .s
24	12, 23	cfv 5888	. . . . . . . . 9 class ( .s ` s )
25	20, 22, 24	co 6650	. . . . . . . 8 class ( z ( .s ` s ) ( 1r ` s ) )
26	9	cv 1482	. . . . . . . . 9 class i
27		cqg 17590	. . . . . . . . 9 class ~QG
28	12, 26, 27	co 6650	. . . . . . . 8 class ( s ~QG i )
29	25, 28	cec 7740	. . . . . . 7 class [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i )
30	17, 19, 29	cmpt 4729	. . . . . 6 class ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) )
31		vt	. . . . . . . 8 setvar t
32		cqus 16165	. . . . . . . . 9 class /.s
33	12, 28, 32	co 6650	. . . . . . . 8 class ( s /.s ( s ~QG i ) )
34	31	cv 1482	. . . . . . . . . 10 class t
35		vn	. . . . . . . . . . . . . 14 setvar n
36	35	cv 1482	. . . . . . . . . . . . 13 class n
37	16	cv 1482	. . . . . . . . . . . . 13 class f
38	36, 37	ccom 5118	. . . . . . . . . . . 12 class ( n o. f )
39		cnm 22381	. . . . . . . . . . . . 13 class norm
40	6, 39	cfv 5888	. . . . . . . . . . . 12 class ( norm ` r )
41	38, 40	wceq 1483	. . . . . . . . . . 11 wff ( n o. f ) = ( norm ` r )
42		cabv 18816	. . . . . . . . . . . 12 class AbsVal
43	34, 42	cfv 5888	. . . . . . . . . . 11 class (AbsVal ` t )
44	41, 35, 43	crio 6610	. . . . . . . . . 10 class ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) )
45		ctng 22383	. . . . . . . . . 10 class toNrmGrp
46	34, 44, 45	co 6650	. . . . . . . . 9 class ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) )
47		cnx 15854	. . . . . . . . . . 11 class ndx
48		cple 15948	. . . . . . . . . . 11 class le
49	47, 48	cfv 5888	. . . . . . . . . 10 class ( le ` ndx )
50		vg	. . . . . . . . . . 11 setvar g
51	34, 18	cfv 5888	. . . . . . . . . . . 12 class ( Base ` t )
52		vq	. . . . . . . . . . . . . . . 16 setvar q
53	52	cv 1482	. . . . . . . . . . . . . . 15 class q
54		cdg1 23814	. . . . . . . . . . . . . . 15 class deg1
55	6, 53, 54	co 6650	. . . . . . . . . . . . . 14 class ( r deg1 q )
56	6, 10, 54	co 6650	. . . . . . . . . . . . . 14 class ( r deg1 p )
57		clt 10074	. . . . . . . . . . . . . 14 class <
58	55, 56, 57	wbr 4653	. . . . . . . . . . . . 13 wff ( r deg1 q ) < ( r deg1 p )
59	58, 52, 20	crio 6610	. . . . . . . . . . . 12 class ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) )
60	17, 51, 59	cmpt 4729	. . . . . . . . . . 11 class ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) )
61	50	cv 1482	. . . . . . . . . . . . 13 class g
62	61	ccnv 5113	. . . . . . . . . . . 12 class `' g
63	12, 48	cfv 5888	. . . . . . . . . . . . 13 class ( le ` s )
64	63, 61	ccom 5118	. . . . . . . . . . . 12 class ( ( le ` s ) o. g )
65	62, 64	ccom 5118	. . . . . . . . . . 11 class ( `' g o. ( ( le ` s ) o. g ) )
66	50, 60, 65	csb 3533	. . . . . . . . . 10 class [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) )
67	49, 66	cop 4183	. . . . . . . . 9 class <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >.
68		csts 15855	. . . . . . . . 9 class sSet
69	46, 67, 68	co 6650	. . . . . . . 8 class ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. )
70	31, 33, 69	csb 3533	. . . . . . 7 class [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. )
71	70, 37	cop 4183	. . . . . 6 class <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >.
72	16, 30, 71	csb 3533	. . . . 5 class [_ ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_ <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >.
73	9, 15, 72	csb 3533	. . . 4 class [_ ( (RSpan ` s ) ` { p } ) / i ]_ [_ ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_ <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >.
74	5, 8, 73	csb 3533	. . 3 class [_ (Poly1 ` r ) / s ]_ [_ ( (RSpan ` s ) ` { p } ) / i ]_ [_ ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_ <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >.
75	2, 3, 4, 4, 74	cmpt2 6652	. 2 class ( r e. _V , p e. _V |-> [_ (Poly1 ` r ) / s ]_ [_ ( (RSpan ` s ) ` { p } ) / i ]_ [_ ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_ <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >. )
76	1, 75	wceq 1483	1 wff polyFld = ( r e. _V , p e. _V |-> [_ (Poly1 ` r ) / s ]_ [_ ( (RSpan ` s ) ` { p } ) / i ]_ [_ ( z e. ( Base ` r ) |-> [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_ <. [_ ( s /.s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e. (AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) , [_ ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_ ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >. )

This definition is referenced by: (None)