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 = ( 𝑟 ∈ V , 𝑝 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( ( RSpan ‘ 𝑠 ) ‘ { 𝑝 } ) / 𝑖 ⦌ ⦋ ( 𝑐 ∈ ( Base ‘ 𝑟 ) ↦ [ ( 𝑐 ( ·𝑠 ‘ 𝑠 ) ( 1r ‘ 𝑠 ) ) ] ( 𝑠 ~QG 𝑖 ) ) / 𝑓 ⦌ ⟨ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑞 ( rem1p ‘ 𝑟 ) 𝑝 ) = 𝑞 ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ ) , 𝑓 ⟩ )

Detailed syntax breakdown

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