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 = (r \in V, p \in V ⟼ ⦋ {Poly}_{1} (r) / s ⦌ ⦋ RSpan (s) (\{p\}) / i ⦌ ⦋ (z \in {Base}_{r} ⟼ [(z \cdot_{s} 1_{s})] (s ~_{QG} i)) / f ⦌ ⟨⦋ (s /_{𝑠} (s ~_{QG} i)) / t ⦌ ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩), f⟩)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpfl	$class polyFld$
1		vr	$setvar r$
2		cvv	$class V$
3		vp	$setvar p$
4		cpl1	$class {Poly}_{1}$
5	1	cv	$setvar r$
6	5 4	cfv	$class {Poly}_{1} (r)$
7		vs	$setvar s$
8		crsp	$class RSpan$
9	7	cv	$setvar s$
10	9 8	cfv	$class RSpan (s)$
11	3	cv	$setvar p$
12	11	csn	$class \{p\}$
13	12 10	cfv	$class RSpan (s) (\{p\})$
14		vi	$setvar i$
15		vz	$setvar z$
16		cbs	$class Base$
17	5 16	cfv	$class {Base}_{r}$
18	15	cv	$setvar z$
19		cvsca	$class \cdot_{𝑠}$
20	9 19	cfv	$class \cdot_{s}$
21		cur	$class 1_{r}$
22	9 21	cfv	$class 1_{s}$
23	18 22 20	co	$class (z \cdot_{s} 1_{s})$
24		cqg	$class ~_{QG}$
25	14	cv	$setvar i$
26	9 25 24	co	$class (s ~_{QG} i)$
27	23 26	cec	$class [(z \cdot_{s} 1_{s})] (s ~_{QG} i)$
28	15 17 27	cmpt	$class (z \in {Base}_{r} ⟼ [(z \cdot_{s} 1_{s})] (s ~_{QG} i))$
29		vf	$setvar f$
30		cqus	$class /_{𝑠}$
31	9 26 30	co	$class (s /_{𝑠} (s ~_{QG} i))$
32		vt	$setvar t$
33	32	cv	$setvar t$
34		ctng	$class toNrmGrp$
35		vn	$setvar n$
36		cabv	$class AbsVal$
37	33 36	cfv	$class AbsVal (t)$
38	35	cv	$setvar n$
39	29	cv	$setvar f$
40	38 39	ccom	$class (n \circ f)$
41		cnm	$class norm$
42	5 41	cfv	$class norm (r)$
43	40 42	wceq	$wff n \circ f = norm (r)$
44	43 35 37	crio	$class (ι n \in AbsVal (t) \| n \circ f = norm (r))$
45	33 44 34	co	$class (t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r)))$
46		csts	$class sSet$
47		cple	$class le$
48		cnx	$class ndx$
49	48 47	cfv	$class \leq_{ndx}$
50	33 16	cfv	$class {Base}_{t}$
51		vq	$setvar q$
52		cdg1	$class \deg_{1}$
53	51	cv	$setvar q$
54	5 53 52	co	$class (r \deg_{1} q)$
55		clt	$class <$
56	5 11 52	co	$class (r \deg_{1} p)$
57	54 56 55	wbr	$wff r \deg_{1} q < r \deg_{1} p$
58	57 51 18	crio	$class (ι q \in z \| r \deg_{1} q < r \deg_{1} p)$
59	15 50 58	cmpt	$class (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p))$
60		vg	$setvar g$
61	60	cv	$setvar g$
62	61	ccnv	$class g^{-1}$
63	9 47	cfv	$class \leq_{s}$
64	63 61	ccom	$class (\leq_{s} \circ g)$
65	62 64	ccom	$class (g^{-1} \circ (\leq_{s} \circ g))$
66	60 59 65	csb	$class ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))$
67	49 66	cop	$class ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩$
68	45 67 46	co	$class ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩)$
69	32 31 68	csb	$class ⦋ (s /_{𝑠} (s ~_{QG} i)) / t ⦌ ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩)$
70	69 39	cop	$class ⟨⦋ (s /_{𝑠} (s ~_{QG} i)) / t ⦌ ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩), f⟩$
71	29 28 70	csb	$class ⦋ (z \in {Base}_{r} ⟼ [(z \cdot_{s} 1_{s})] (s ~_{QG} i)) / f ⦌ ⟨⦋ (s /_{𝑠} (s ~_{QG} i)) / t ⦌ ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩), f⟩$
72	14 13 71	csb	$class ⦋ RSpan (s) (\{p\}) / i ⦌ ⦋ (z \in {Base}_{r} ⟼ [(z \cdot_{s} 1_{s})] (s ~_{QG} i)) / f ⦌ ⟨⦋ (s /_{𝑠} (s ~_{QG} i)) / t ⦌ ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩), f⟩$
73	7 6 72	csb	$class ⦋ {Poly}_{1} (r) / s ⦌ ⦋ RSpan (s) (\{p\}) / i ⦌ ⦋ (z \in {Base}_{r} ⟼ [(z \cdot_{s} 1_{s})] (s ~_{QG} i)) / f ⦌ ⟨⦋ (s /_{𝑠} (s ~_{QG} i)) / t ⦌ ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩), f⟩$
74	1 3 2 2 73	cmpo	$class (r \in V, p \in V ⟼ ⦋ {Poly}_{1} (r) / s ⦌ ⦋ RSpan (s) (\{p\}) / i ⦌ ⦋ (z \in {Base}_{r} ⟼ [(z \cdot_{s} 1_{s})] (s ~_{QG} i)) / f ⦌ ⟨⦋ (s /_{𝑠} (s ~_{QG} i)) / t ⦌ ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩), f⟩)$
75	0 74	wceq	$wff polyFld = (r \in V, p \in V ⟼ ⦋ {Poly}_{1} (r) / s ⦌ ⦋ RSpan (s) (\{p\}) / i ⦌ ⦋ (z \in {Base}_{r} ⟼ [(z \cdot_{s} 1_{s})] (s ~_{QG} i)) / f ⦌ ⟨⦋ (s /_{𝑠} (s ~_{QG} i)) / t ⦌ ((t toNrmGrp (ι n \in AbsVal (t) \| n \circ f = norm (r))) sSet ⟨\leq_{ndx}, ⦋ (z \in {Base}_{t} ⟼ (ι q \in z \| r \deg_{1} q < r \deg_{1} p)) / g ⦌ (g^{-1} \circ (\leq_{s} \circ g))⟩), f⟩)$

Metamath Proof Explorer

Definition df-plfl

Detailed syntax breakdown