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