Definition df-plfl 35643

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.)

Assertion

Ref	Expression
df-plfl	⊢ polyFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)

Distinct variable group:   𝑓,𝑐,𝑔,𝑖,𝑛,𝑝,𝑞,𝑟,𝑠,𝑡,𝑧

Detailed syntax breakdown of Definition df-plfl

Step	Hyp	Ref	Expression
1		cpfl 35636	. 2 class polyFld
2		vr	. . 3 setvar 𝑟
3		vp	. . 3 setvar 𝑝
4		cvv 3479	. . 3 class V
5		vs	. . . 4 setvar 𝑠
6	2	cv 1538	. . . . 5 class 𝑟
7		cpl1 22179	. . . . 5 class Poly1
8	6, 7	cfv 6560	. . . 4 class (Poly1‘𝑟)
9		vi	. . . . 5 setvar 𝑖
10	3	cv 1538	. . . . . . 7 class 𝑝
11	10	csn 4625	. . . . . 6 class {𝑝}
12	5	cv 1538	. . . . . . 7 class 𝑠
13		crsp 21218	. . . . . . 7 class RSpan
14	12, 13	cfv 6560	. . . . . 6 class (RSpan‘𝑠)
15	11, 14	cfv 6560	. . . . 5 class ((RSpan‘𝑠)‘{𝑝})
16		vf	. . . . . 6 setvar 𝑓
17		vc	. . . . . . 7 setvar 𝑐
18		cbs 17248	. . . . . . . 8 class Base
19	6, 18	cfv 6560	. . . . . . 7 class (Base‘𝑟)
20	17	cv 1538	. . . . . . . . 9 class 𝑐
21		cur 20179	. . . . . . . . . 10 class 1r
22	12, 21	cfv 6560	. . . . . . . . 9 class (1r‘𝑠)
23		cvsca 17302	. . . . . . . . . 10 class ·𝑠
24	12, 23	cfv 6560	. . . . . . . . 9 class ( ·𝑠 ‘𝑠)
25	20, 22, 24	co 7432	. . . . . . . 8 class (𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))
26	9	cv 1538	. . . . . . . . 9 class 𝑖
27		cqg 19141	. . . . . . . . 9 class ~QG
28	12, 26, 27	co 7432	. . . . . . . 8 class (𝑠 ~QG 𝑖)
29	25, 28	cec 8744	. . . . . . 7 class [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)
30	17, 19, 29	cmpt 5224	. . . . . 6 class (𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖))
31		vt	. . . . . . . 8 setvar 𝑡
32		cqus 17551	. . . . . . . . 9 class /s
33	12, 28, 32	co 7432	. . . . . . . 8 class (𝑠 /s (𝑠 ~QG 𝑖))
34	31	cv 1538	. . . . . . . . . 10 class 𝑡
35		vn	. . . . . . . . . . . . . 14 setvar 𝑛
36	35	cv 1538	. . . . . . . . . . . . 13 class 𝑛
37	16	cv 1538	. . . . . . . . . . . . 13 class 𝑓
38	36, 37	ccom 5688	. . . . . . . . . . . 12 class (𝑛 ∘ 𝑓)
39		cnm 24590	. . . . . . . . . . . . 13 class norm
40	6, 39	cfv 6560	. . . . . . . . . . . 12 class (norm‘𝑟)
41	38, 40	wceq 1539	. . . . . . . . . . 11 wff (𝑛 ∘ 𝑓) = (norm‘𝑟)
42		cabv 20810	. . . . . . . . . . . 12 class AbsVal
43	34, 42	cfv 6560	. . . . . . . . . . 11 class (AbsVal‘𝑡)
44	41, 35, 43	crio 7388	. . . . . . . . . 10 class (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))
45		ctng 24592	. . . . . . . . . 10 class toNrmGrp
46	34, 44, 45	co 7432	. . . . . . . . 9 class (𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟)))
47		cnx 17231	. . . . . . . . . . 11 class ndx
48		cple 17305	. . . . . . . . . . 11 class le
49	47, 48	cfv 6560	. . . . . . . . . 10 class (le‘ndx)
50		vg	. . . . . . . . . . 11 setvar 𝑔
51		vz	. . . . . . . . . . . 12 setvar 𝑧
52	34, 18	cfv 6560	. . . . . . . . . . . 12 class (Base‘𝑡)
53		vq	. . . . . . . . . . . . . . . 16 setvar 𝑞
54	53	cv 1538	. . . . . . . . . . . . . . 15 class 𝑞
55		cr1p 26169	. . . . . . . . . . . . . . . 16 class rem1p
56	6, 55	cfv 6560	. . . . . . . . . . . . . . 15 class (rem1p‘𝑟)
57	54, 10, 56	co 7432	. . . . . . . . . . . . . 14 class (𝑞(rem1p‘𝑟)𝑝)
58	57, 54	wceq 1539	. . . . . . . . . . . . 13 wff (𝑞(rem1p‘𝑟)𝑝) = 𝑞
59	51	cv 1538	. . . . . . . . . . . . 13 class 𝑧
60	58, 53, 59	crio 7388	. . . . . . . . . . . 12 class (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)
61	51, 52, 60	cmpt 5224	. . . . . . . . . . 11 class (𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞))
62	50	cv 1538	. . . . . . . . . . . . 13 class 𝑔
63	62	ccnv 5683	. . . . . . . . . . . 12 class ◡𝑔
64	12, 48	cfv 6560	. . . . . . . . . . . . 13 class (le‘𝑠)
65	64, 62	ccom 5688	. . . . . . . . . . . 12 class ((le‘𝑠) ∘ 𝑔)
66	63, 65	ccom 5688	. . . . . . . . . . 11 class (◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))
67	50, 61, 66	csb 3898	. . . . . . . . . 10 class ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))
68	49, 67	cop 4631	. . . . . . . . 9 class ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩
69		csts 17201	. . . . . . . . 9 class sSet
70	46, 68, 69	co 7432	. . . . . . . 8 class ((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩)
71	31, 33, 70	csb 3898	. . . . . . 7 class ⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩)
72	71, 37	cop 4631	. . . . . 6 class ⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩
73	16, 30, 72	csb 3898	. . . . 5 class ⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩
74	9, 15, 73	csb 3898	. . . 4 class ⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩
75	5, 8, 74	csb 3898	. . 3 class ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩
76	2, 3, 4, 4, 75	cmpo 7434	. 2 class (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)
77	1, 76	wceq 1539	1 wff polyFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)

This definition is referenced by: (None)