Metamath Proof Explorer


Definition df-plfl

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)

Ref Expression
Assertion df-plfl polyFld = r V , p V Poly 1 r / s RSpan s p / i z Base r z s 1 s s ~ QG i / f s / 𝑠 s ~ QG i / t t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpfl class polyFld
1 vr setvar r
2 cvv class V
3 vp setvar p
4 cpl1 class Poly 1
5 1 cv setvar r
6 5 4 cfv class Poly 1 r
7 vs setvar s
8 crsp class RSpan
9 7 cv setvar s
10 9 8 cfv class RSpan s
11 3 cv setvar p
12 11 csn class p
13 12 10 cfv class RSpan s p
14 vi setvar i
15 vz setvar z
16 cbs class Base
17 5 16 cfv class Base r
18 15 cv setvar z
19 cvsca class 𝑠
20 9 19 cfv class s
21 cur class 1 r
22 9 21 cfv class 1 s
23 18 22 20 co class z s 1 s
24 cqg class ~ QG
25 14 cv setvar i
26 9 25 24 co class s ~ QG i
27 23 26 cec class z s 1 s s ~ QG i
28 15 17 27 cmpt class z Base r z s 1 s s ~ QG i
29 vf setvar f
30 cqus class / 𝑠
31 9 26 30 co class s / 𝑠 s ~ QG i
32 vt setvar t
33 32 cv setvar t
34 ctng class toNrmGrp
35 vn setvar n
36 cabv class AbsVal
37 33 36 cfv class AbsVal t
38 35 cv setvar n
39 29 cv setvar f
40 38 39 ccom class n f
41 cnm class norm
42 5 41 cfv class norm r
43 40 42 wceq wff n f = norm r
44 43 35 37 crio class ι n AbsVal t | n f = norm r
45 33 44 34 co class t toNrmGrp ι n AbsVal t | n f = norm r
46 csts class sSet
47 cple class le
48 cnx class ndx
49 48 47 cfv class ndx
50 33 16 cfv class Base t
51 vq setvar q
52 cdg1 class deg 1
53 51 cv setvar q
54 5 53 52 co class r deg 1 q
55 clt class <
56 5 11 52 co class r deg 1 p
57 54 56 55 wbr wff r deg 1 q < r deg 1 p
58 57 51 18 crio class ι q z | r deg 1 q < r deg 1 p
59 15 50 58 cmpt class z Base t ι q z | r deg 1 q < r deg 1 p
60 vg setvar g
61 60 cv setvar g
62 61 ccnv class g -1
63 9 47 cfv class s
64 63 61 ccom class s g
65 62 64 ccom class g -1 s g
66 60 59 65 csb class z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g
67 49 66 cop class ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g
68 45 67 46 co class t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g
69 32 31 68 csb class s / 𝑠 s ~ QG i / t t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g
70 69 39 cop class s / 𝑠 s ~ QG i / t t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g f
71 29 28 70 csb class z Base r z s 1 s s ~ QG i / f s / 𝑠 s ~ QG i / t t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g f
72 14 13 71 csb class RSpan s p / i z Base r z s 1 s s ~ QG i / f s / 𝑠 s ~ QG i / t t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g f
73 7 6 72 csb class Poly 1 r / s RSpan s p / i z Base r z s 1 s s ~ QG i / f s / 𝑠 s ~ QG i / t t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g f
74 1 3 2 2 73 cmpo class r V , p V Poly 1 r / s RSpan s p / i z Base r z s 1 s s ~ QG i / f s / 𝑠 s ~ QG i / t t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g f
75 0 74 wceq wff polyFld = r V , p V Poly 1 r / s RSpan s p / i z Base r z s 1 s s ~ QG i / f s / 𝑠 s ~ QG i / t t toNrmGrp ι n AbsVal t | n f = norm r sSet ndx z Base t ι q z | r deg 1 q < r deg 1 p / g g -1 s g f