Definition df-plfl 30788

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

Step	Hyp	Ref	Expression
1		cpfl 30780	. 2 class polyFld
2		vr	. . 3 setvar 𝑟
3		vp	. . 3 setvar 𝑝
4		cvv 3173	. . 3 class V
5		vs	. . . 4 setvar 𝑠
6	2	cv 1474	. . . . 5 class 𝑟
7		cpl1 19368	. . . . 5 class Poly1
8	6, 7	cfv 5804	. . . 4 class (Poly1‘𝑟)
9		vi	. . . . 5 setvar 𝑖
10	3	cv 1474	. . . . . . 7 class 𝑝
11	10	csn 4125	. . . . . 6 class {𝑝}
12	5	cv 1474	. . . . . . 7 class 𝑠
13		crsp 18992	. . . . . . 7 class RSpan
14	12, 13	cfv 5804	. . . . . 6 class (RSpan‘𝑠)
15	11, 14	cfv 5804	. . . . 5 class ((RSpan‘𝑠)‘{𝑝})
16		vf	. . . . . 6 setvar 𝑓
17		vz	. . . . . . 7 setvar 𝑧
18		cbs 15695	. . . . . . . 8 class Base
19	6, 18	cfv 5804	. . . . . . 7 class (Base‘𝑟)
20	17	cv 1474	. . . . . . . . 9 class 𝑧
21		cur 18324	. . . . . . . . . 10 class 1r
22	12, 21	cfv 5804	. . . . . . . . 9 class (1r‘𝑠)
23		cvsca 15772	. . . . . . . . . 10 class ·𝑠
24	12, 23	cfv 5804	. . . . . . . . 9 class ( ·𝑠 ‘𝑠)
25	20, 22, 24	co 6549	. . . . . . . 8 class (𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))
26	9	cv 1474	. . . . . . . . 9 class 𝑖
27		cqg 17413	. . . . . . . . 9 class ~QG
28	12, 26, 27	co 6549	. . . . . . . 8 class (𝑠 ~QG 𝑖)
29	25, 28	cec 7627	. . . . . . 7 class [(𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)
30	17, 19, 29	cmpt 4643	. . . . . 6 class (𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖))
31		vt	. . . . . . . 8 setvar 𝑡
32		cqus 15988	. . . . . . . . 9 class /s
33	12, 28, 32	co 6549	. . . . . . . 8 class (𝑠 /s (𝑠 ~QG 𝑖))
34	31	cv 1474	. . . . . . . . . 10 class 𝑡
35		vn	. . . . . . . . . . . . . 14 setvar 𝑛
36	35	cv 1474	. . . . . . . . . . . . 13 class 𝑛
37	16	cv 1474	. . . . . . . . . . . . 13 class 𝑓
38	36, 37	ccom 5042	. . . . . . . . . . . 12 class (𝑛 ∘ 𝑓)
39		cnm 22191	. . . . . . . . . . . . 13 class norm
40	6, 39	cfv 5804	. . . . . . . . . . . 12 class (norm‘𝑟)
41	38, 40	wceq 1475	. . . . . . . . . . 11 wff (𝑛 ∘ 𝑓) = (norm‘𝑟)
42		cabv 18639	. . . . . . . . . . . 12 class AbsVal
43	34, 42	cfv 5804	. . . . . . . . . . 11 class (AbsVal‘𝑡)
44	41, 35, 43	crio 6510	. . . . . . . . . 10 class (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))
45		ctng 22193	. . . . . . . . . 10 class toNrmGrp
46	34, 44, 45	co 6549	. . . . . . . . 9 class (𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟)))
47		cnx 15692	. . . . . . . . . . 11 class ndx
48		cple 15775	. . . . . . . . . . 11 class le
49	47, 48	cfv 5804	. . . . . . . . . 10 class (le‘ndx)
50		vg	. . . . . . . . . . 11 setvar 𝑔
51	34, 18	cfv 5804	. . . . . . . . . . . 12 class (Base‘𝑡)
52		vq	. . . . . . . . . . . . . . . 16 setvar 𝑞
53	52	cv 1474	. . . . . . . . . . . . . . 15 class 𝑞
54		cdg1 23618	. . . . . . . . . . . . . . 15 class deg1
55	6, 53, 54	co 6549	. . . . . . . . . . . . . 14 class (𝑟 deg1 𝑞)
56	6, 10, 54	co 6549	. . . . . . . . . . . . . 14 class (𝑟 deg1 𝑝)
57		clt 9953	. . . . . . . . . . . . . 14 class <
58	55, 56, 57	wbr 4583	. . . . . . . . . . . . 13 wff (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝)
59	58, 52, 20	crio 6510	. . . . . . . . . . . 12 class (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))
60	17, 51, 59	cmpt 4643	. . . . . . . . . . 11 class (𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝)))
61	50	cv 1474	. . . . . . . . . . . . 13 class 𝑔
62	61	ccnv 5037	. . . . . . . . . . . 12 class ◡𝑔
63	12, 48	cfv 5804	. . . . . . . . . . . . 13 class (le‘𝑠)
64	63, 61	ccom 5042	. . . . . . . . . . . 12 class ((le‘𝑠) ∘ 𝑔)
65	62, 64	ccom 5042	. . . . . . . . . . 11 class (◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))
66	50, 60, 65	csb 3499	. . . . . . . . . 10 class ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))
67	49, 66	cop 4131	. . . . . . . . 9 class ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩
68		csts 15693	. . . . . . . . 9 class sSet
69	46, 67, 68	co 6549	. . . . . . . 8 class ((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩)
70	31, 33, 69	csb 3499	. . . . . . 7 class ⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩)
71	70, 37	cop 4131	. . . . . 6 class ⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩
72	16, 30, 71	csb 3499	. . . . 5 class ⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩
73	9, 15, 72	csb 3499	. . . 4 class ⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩
74	5, 8, 73	csb 3499	. . 3 class ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩
75	2, 3, 4, 4, 74	cmpt2 6551	. 2 class (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)
76	1, 75	wceq 1475	1 wff polyFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)

This definition is referenced by: (None)