Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-plfl Structured version   Visualization version   GIF version

Definition df-plfl 33337
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 = (𝑟 ∈ V, 𝑝 ∈ V ↦ (Poly1𝑟) / 𝑠((RSpan‘𝑠)‘{𝑝}) / 𝑖(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠𝑠)(1r𝑠))](𝑠 ~QG 𝑖)) / 𝑓(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)
Distinct variable group:   𝑓,𝑔,𝑖,𝑛,𝑝,𝑞,𝑟,𝑠,𝑡,𝑧

Detailed syntax breakdown of Definition df-plfl
StepHypRef Expression
1 cpfl 33329 . 2 class polyFld
2 vr . . 3 setvar 𝑟
3 vp . . 3 setvar 𝑝
4 cvv 3421 . . 3 class V
5 vs . . . 4 setvar 𝑠
62cv 1542 . . . . 5 class 𝑟
7 cpl1 21122 . . . . 5 class Poly1
86, 7cfv 6398 . . . 4 class (Poly1𝑟)
9 vi . . . . 5 setvar 𝑖
103cv 1542 . . . . . . 7 class 𝑝
1110csn 4556 . . . . . 6 class {𝑝}
125cv 1542 . . . . . . 7 class 𝑠
13 crsp 20233 . . . . . . 7 class RSpan
1412, 13cfv 6398 . . . . . 6 class (RSpan‘𝑠)
1511, 14cfv 6398 . . . . 5 class ((RSpan‘𝑠)‘{𝑝})
16 vf . . . . . 6 setvar 𝑓
17 vz . . . . . . 7 setvar 𝑧
18 cbs 16785 . . . . . . . 8 class Base
196, 18cfv 6398 . . . . . . 7 class (Base‘𝑟)
2017cv 1542 . . . . . . . . 9 class 𝑧
21 cur 19541 . . . . . . . . . 10 class 1r
2212, 21cfv 6398 . . . . . . . . 9 class (1r𝑠)
23 cvsca 16831 . . . . . . . . . 10 class ·𝑠
2412, 23cfv 6398 . . . . . . . . 9 class ( ·𝑠𝑠)
2520, 22, 24co 7232 . . . . . . . 8 class (𝑧( ·𝑠𝑠)(1r𝑠))
269cv 1542 . . . . . . . . 9 class 𝑖
27 cqg 18564 . . . . . . . . 9 class ~QG
2812, 26, 27co 7232 . . . . . . . 8 class (𝑠 ~QG 𝑖)
2925, 28cec 8410 . . . . . . 7 class [(𝑧( ·𝑠𝑠)(1r𝑠))](𝑠 ~QG 𝑖)
3017, 19, 29cmpt 5150 . . . . . 6 class (𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠𝑠)(1r𝑠))](𝑠 ~QG 𝑖))
31 vt . . . . . . . 8 setvar 𝑡
32 cqus 17035 . . . . . . . . 9 class /s
3312, 28, 32co 7232 . . . . . . . 8 class (𝑠 /s (𝑠 ~QG 𝑖))
3431cv 1542 . . . . . . . . . 10 class 𝑡
35 vn . . . . . . . . . . . . . 14 setvar 𝑛
3635cv 1542 . . . . . . . . . . . . 13 class 𝑛
3716cv 1542 . . . . . . . . . . . . 13 class 𝑓
3836, 37ccom 5570 . . . . . . . . . . . 12 class (𝑛𝑓)
39 cnm 23498 . . . . . . . . . . . . 13 class norm
406, 39cfv 6398 . . . . . . . . . . . 12 class (norm‘𝑟)
4138, 40wceq 1543 . . . . . . . . . . 11 wff (𝑛𝑓) = (norm‘𝑟)
42 cabv 19877 . . . . . . . . . . . 12 class AbsVal
4334, 42cfv 6398 . . . . . . . . . . 11 class (AbsVal‘𝑡)
4441, 35, 43crio 7188 . . . . . . . . . 10 class (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))
45 ctng 23500 . . . . . . . . . 10 class toNrmGrp
4634, 44, 45co 7232 . . . . . . . . 9 class (𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟)))
47 cnx 16769 . . . . . . . . . . 11 class ndx
48 cple 16834 . . . . . . . . . . 11 class le
4947, 48cfv 6398 . . . . . . . . . 10 class (le‘ndx)
50 vg . . . . . . . . . . 11 setvar 𝑔
5134, 18cfv 6398 . . . . . . . . . . . 12 class (Base‘𝑡)
52 vq . . . . . . . . . . . . . . . 16 setvar 𝑞
5352cv 1542 . . . . . . . . . . . . . . 15 class 𝑞
54 cdg1 24973 . . . . . . . . . . . . . . 15 class deg1
556, 53, 54co 7232 . . . . . . . . . . . . . 14 class (𝑟 deg1 𝑞)
566, 10, 54co 7232 . . . . . . . . . . . . . 14 class (𝑟 deg1 𝑝)
57 clt 10892 . . . . . . . . . . . . . 14 class <
5855, 56, 57wbr 5068 . . . . . . . . . . . . 13 wff (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝)
5958, 52, 20crio 7188 . . . . . . . . . . . 12 class (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))
6017, 51, 59cmpt 5150 . . . . . . . . . . 11 class (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝)))
6150cv 1542 . . . . . . . . . . . . 13 class 𝑔
6261ccnv 5565 . . . . . . . . . . . 12 class 𝑔
6312, 48cfv 6398 . . . . . . . . . . . . 13 class (le‘𝑠)
6463, 61ccom 5570 . . . . . . . . . . . 12 class ((le‘𝑠) ∘ 𝑔)
6562, 64ccom 5570 . . . . . . . . . . 11 class (𝑔 ∘ ((le‘𝑠) ∘ 𝑔))
6650, 60, 65csb 3826 . . . . . . . . . 10 class (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))
6749, 66cop 4562 . . . . . . . . 9 class ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩
68 csts 16741 . . . . . . . . 9 class sSet
6946, 67, 68co 7232 . . . . . . . 8 class ((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩)
7031, 33, 69csb 3826 . . . . . . 7 class (𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩)
7170, 37cop 4562 . . . . . 6 class (𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓
7216, 30, 71csb 3826 . . . . 5 class (𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠𝑠)(1r𝑠))](𝑠 ~QG 𝑖)) / 𝑓(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓
739, 15, 72csb 3826 . . . 4 class ((RSpan‘𝑠)‘{𝑝}) / 𝑖(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠𝑠)(1r𝑠))](𝑠 ~QG 𝑖)) / 𝑓(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓
745, 8, 73csb 3826 . . 3 class (Poly1𝑟) / 𝑠((RSpan‘𝑠)‘{𝑝}) / 𝑖(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠𝑠)(1r𝑠))](𝑠 ~QG 𝑖)) / 𝑓(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓
752, 3, 4, 4, 74cmpo 7234 . 2 class (𝑟 ∈ V, 𝑝 ∈ V ↦ (Poly1𝑟) / 𝑠((RSpan‘𝑠)‘{𝑝}) / 𝑖(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠𝑠)(1r𝑠))](𝑠 ~QG 𝑖)) / 𝑓(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)
761, 75wceq 1543 1 wff polyFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ (Poly1𝑟) / 𝑠((RSpan‘𝑠)‘{𝑝}) / 𝑖(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠𝑠)(1r𝑠))](𝑠 ~QG 𝑖)) / 𝑓(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡((𝑡 toNrmGrp (𝑛 ∈ (AbsVal‘𝑡)(𝑛𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), (𝑧 ∈ (Base‘𝑡) ↦ (𝑞𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔(𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator