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) (Revised by Thierry Arnoux and Steven Nguyen, 21-Jun-2025)

Ref Expression
Assertion df-plfl ⊢ polyFld = r ∈ V , p ∈ V ⟼ ⦋ Poly 1 ⁡ r / s⦌ ⦋ RSpan ⁡ s ⁡ p / i⦌ ⦋ c ∈ Base r ⟼ c ⋅ 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 | q rem 1p ⁡ r p = q / 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 vc setvar c
16 cbs class Base
17 5 16 cfv class Base r
18 15 cv setvar c
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 c ⋅ 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 c ⋅ s 1 s s ~ QG i
28 15 17 27 cmpt class c ∈ Base r ⟼ c ⋅ 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 vz setvar z
51 33 16 cfv class Base t
52 vq setvar q
53 50 cv setvar z
54 52 cv setvar q
55 cr1p class rem 1p
56 5 55 cfv class rem 1p ⁡ r
57 54 11 56 co class q rem 1p ⁡ r p
58 57 54 wceq wff q rem 1p ⁡ r p = q
59 58 52 53 crio class ι q ∈ z | q rem 1p ⁡ r p = q
60 50 51 59 cmpt class z ∈ Base t ⟼ ι q ∈ z | q rem 1p ⁡ r p = q
61 vg setvar g
62 61 cv setvar g
63 62 ccnv class g -1
64 9 47 cfv class ≤ s
65 64 62 ccom class ≤ s ∘ g
66 63 65 ccom class g -1 ∘ ≤ s ∘ g
67 61 60 66 csb class ⦋ z ∈ Base t ⟼ ι q ∈ z | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g
68 49 67 cop class ≤ ndx ⦋ z ∈ Base t ⟼ ι q ∈ z | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g
69 45 68 46 co class t toNrmGrp ι n ∈ AbsVal ⁡ t | n ∘ f = norm ⁡ r sSet ≤ ndx ⦋ z ∈ Base t ⟼ ι q ∈ z | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g
70 32 31 69 csb class ⦋ s / 𝑠 s ~ QG i / t⦌ t toNrmGrp ι n ∈ AbsVal ⁡ t | n ∘ f = norm ⁡ r sSet ≤ ndx ⦋ z ∈ Base t ⟼ ι q ∈ z | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g
71 70 39 cop class ⦋ s / 𝑠 s ~ QG i / t⦌ t toNrmGrp ι n ∈ AbsVal ⁡ t | n ∘ f = norm ⁡ r sSet ≤ ndx ⦋ z ∈ Base t ⟼ ι q ∈ z | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g f
72 29 28 71 csb class ⦋ c ∈ Base r ⟼ c ⋅ 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 | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g f
73 14 13 72 csb class ⦋ RSpan ⁡ s ⁡ p / i⦌ ⦋ c ∈ Base r ⟼ c ⋅ 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 | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g f
74 7 6 73 csb class ⦋ Poly 1 ⁡ r / s⦌ ⦋ RSpan ⁡ s ⁡ p / i⦌ ⦋ c ∈ Base r ⟼ c ⋅ 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 | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g f
75 1 3 2 2 74 cmpo class r ∈ V , p ∈ V ⟼ ⦋ Poly 1 ⁡ r / s⦌ ⦋ RSpan ⁡ s ⁡ p / i⦌ ⦋ c ∈ Base r ⟼ c ⋅ 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 | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g f
76 0 75 wceq wff polyFld = r ∈ V , p ∈ V ⟼ ⦋ Poly 1 ⁡ r / s⦌ ⦋ RSpan ⁡ s ⁡ p / i⦌ ⦋ c ∈ Base r ⟼ c ⋅ 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 | q rem 1p ⁡ r p = q / g⦌ g -1 ∘ ≤ s ∘ g f