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)

	Ref	Expression
Assertion	df-plfl	⊢ polyFld = ( 𝑟 ∈ V , 𝑝 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( ( RSpan ‘ 𝑠 ) ‘ { 𝑝 } ) / 𝑖 ⦌ ⦋ ( 𝑧 ∈ ( Base ‘ 𝑟 ) ↦ [ ( 𝑧 ( ·𝑠 ‘ 𝑠 ) ( 1r ‘ 𝑠 ) ) ] ( 𝑠 ~QG 𝑖 ) ) / 𝑓 ⦌ ⟨ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( 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		vz	⊢ 𝑧
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	33 16	cfv	⊢ ( Base ‘ 𝑡 )
51		vq	⊢ 𝑞
52		cdg1	⊢ deg1
53	51	cv	⊢ 𝑞
54	5 53 52	co	⊢ ( 𝑟 deg1 𝑞 )
55		clt	⊢ <
56	5 11 52	co	⊢ ( 𝑟 deg1 𝑝 )
57	54 56 55	wbr	⊢ ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 )
58	57 51 18	crio	⊢ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) )
59	15 50 58	cmpt	⊢ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) )
60		vg	⊢ 𝑔
61	60	cv	⊢ 𝑔
62	61	ccnv	⊢ ◡ 𝑔
63	9 47	cfv	⊢ ( le ‘ 𝑠 )
64	63 61	ccom	⊢ ( ( le ‘ 𝑠 ) ∘ 𝑔 )
65	62 64	ccom	⊢ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) )
66	60 59 65	csb	⊢ ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) )
67	49 66	cop	⊢ ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩
68	45 67 46	co	⊢ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ )
69	32 31 68	csb	⊢ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ )
70	69 39	cop	⊢ ⟨ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ ) , 𝑓 ⟩
71	29 28 70	csb	⊢ ⦋ ( 𝑧 ∈ ( Base ‘ 𝑟 ) ↦ [ ( 𝑧 ( ·𝑠 ‘ 𝑠 ) ( 1r ‘ 𝑠 ) ) ] ( 𝑠 ~QG 𝑖 ) ) / 𝑓 ⦌ ⟨ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ ) , 𝑓 ⟩
72	14 13 71	csb	⊢ ⦋ ( ( RSpan ‘ 𝑠 ) ‘ { 𝑝 } ) / 𝑖 ⦌ ⦋ ( 𝑧 ∈ ( Base ‘ 𝑟 ) ↦ [ ( 𝑧 ( ·𝑠 ‘ 𝑠 ) ( 1r ‘ 𝑠 ) ) ] ( 𝑠 ~QG 𝑖 ) ) / 𝑓 ⦌ ⟨ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ ) , 𝑓 ⟩
73	7 6 72	csb	⊢ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( ( RSpan ‘ 𝑠 ) ‘ { 𝑝 } ) / 𝑖 ⦌ ⦋ ( 𝑧 ∈ ( Base ‘ 𝑟 ) ↦ [ ( 𝑧 ( ·𝑠 ‘ 𝑠 ) ( 1r ‘ 𝑠 ) ) ] ( 𝑠 ~QG 𝑖 ) ) / 𝑓 ⦌ ⟨ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ ) , 𝑓 ⟩
74	1 3 2 2 73	cmpo	⊢ ( 𝑟 ∈ V , 𝑝 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( ( RSpan ‘ 𝑠 ) ‘ { 𝑝 } ) / 𝑖 ⦌ ⦋ ( 𝑧 ∈ ( Base ‘ 𝑟 ) ↦ [ ( 𝑧 ( ·𝑠 ‘ 𝑠 ) ( 1r ‘ 𝑠 ) ) ] ( 𝑠 ~QG 𝑖 ) ) / 𝑓 ⦌ ⟨ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ ) , 𝑓 ⟩ )
75	0 74	wceq	⊢ polyFld = ( 𝑟 ∈ V , 𝑝 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑠 ⦌ ⦋ ( ( RSpan ‘ 𝑠 ) ‘ { 𝑝 } ) / 𝑖 ⦌ ⦋ ( 𝑧 ∈ ( Base ‘ 𝑟 ) ↦ [ ( 𝑧 ( ·𝑠 ‘ 𝑠 ) ( 1r ‘ 𝑠 ) ) ] ( 𝑠 ~QG 𝑖 ) ) / 𝑓 ⦌ ⟨ ⦋ ( 𝑠 /s ( 𝑠 ~QG 𝑖 ) ) / 𝑡 ⦌ ( ( 𝑡 toNrmGrp ( ℩ 𝑛 ∈ ( AbsVal ‘ 𝑡 ) ( 𝑛 ∘ 𝑓 ) = ( norm ‘ 𝑟 ) ) ) sSet ⟨ ( le ‘ ndx ) , ⦋ ( 𝑧 ∈ ( Base ‘ 𝑡 ) ↦ ( ℩ 𝑞 ∈ 𝑧 ( 𝑟 deg1 𝑞 ) < ( 𝑟 deg1 𝑝 ) ) ) / 𝑔 ⦌ ( ◡ 𝑔 ∘ ( ( le ‘ 𝑠 ) ∘ 𝑔 ) ) ⟩ ) , 𝑓 ⟩ )