Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-plfl Structured version   Visualization version   GIF version

Definition df-plfl 34623
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
StepHypRef Expression
1 cpfl 34616 . 2 class polyFld
2 vr . . 3 setvar π‘Ÿ
3 vp . . 3 setvar 𝑝
4 cvv 3474 . . 3 class V
5 vs . . . 4 setvar 𝑠
62cv 1540 . . . . 5 class π‘Ÿ
7 cpl1 21700 . . . . 5 class Poly1
86, 7cfv 6543 . . . 4 class (Poly1β€˜π‘Ÿ)
9 vi . . . . 5 setvar 𝑖
103cv 1540 . . . . . . 7 class 𝑝
1110csn 4628 . . . . . 6 class {𝑝}
125cv 1540 . . . . . . 7 class 𝑠
13 crsp 20783 . . . . . . 7 class RSpan
1412, 13cfv 6543 . . . . . 6 class (RSpanβ€˜π‘ )
1511, 14cfv 6543 . . . . 5 class ((RSpanβ€˜π‘ )β€˜{𝑝})
16 vf . . . . . 6 setvar 𝑓
17 vz . . . . . . 7 setvar 𝑧
18 cbs 17143 . . . . . . . 8 class Base
196, 18cfv 6543 . . . . . . 7 class (Baseβ€˜π‘Ÿ)
2017cv 1540 . . . . . . . . 9 class 𝑧
21 cur 20003 . . . . . . . . . 10 class 1r
2212, 21cfv 6543 . . . . . . . . 9 class (1rβ€˜π‘ )
23 cvsca 17200 . . . . . . . . . 10 class ·𝑠
2412, 23cfv 6543 . . . . . . . . 9 class ( ·𝑠 β€˜π‘ )
2520, 22, 24co 7408 . . . . . . . 8 class (𝑧( ·𝑠 β€˜π‘ )(1rβ€˜π‘ ))
269cv 1540 . . . . . . . . 9 class 𝑖
27 cqg 19001 . . . . . . . . 9 class ~QG
2812, 26, 27co 7408 . . . . . . . 8 class (𝑠 ~QG 𝑖)
2925, 28cec 8700 . . . . . . 7 class [(𝑧( ·𝑠 β€˜π‘ )(1rβ€˜π‘ ))](𝑠 ~QG 𝑖)
3017, 19, 29cmpt 5231 . . . . . 6 class (𝑧 ∈ (Baseβ€˜π‘Ÿ) ↦ [(𝑧( ·𝑠 β€˜π‘ )(1rβ€˜π‘ ))](𝑠 ~QG 𝑖))
31 vt . . . . . . . 8 setvar 𝑑
32 cqus 17450 . . . . . . . . 9 class /s
3312, 28, 32co 7408 . . . . . . . 8 class (𝑠 /s (𝑠 ~QG 𝑖))
3431cv 1540 . . . . . . . . . 10 class 𝑑
35 vn . . . . . . . . . . . . . 14 setvar 𝑛
3635cv 1540 . . . . . . . . . . . . 13 class 𝑛
3716cv 1540 . . . . . . . . . . . . 13 class 𝑓
3836, 37ccom 5680 . . . . . . . . . . . 12 class (𝑛 ∘ 𝑓)
39 cnm 24084 . . . . . . . . . . . . 13 class norm
406, 39cfv 6543 . . . . . . . . . . . 12 class (normβ€˜π‘Ÿ)
4138, 40wceq 1541 . . . . . . . . . . 11 wff (𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ)
42 cabv 20423 . . . . . . . . . . . 12 class AbsVal
4334, 42cfv 6543 . . . . . . . . . . 11 class (AbsValβ€˜π‘‘)
4441, 35, 43crio 7363 . . . . . . . . . 10 class (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))
45 ctng 24086 . . . . . . . . . 10 class toNrmGrp
4634, 44, 45co 7408 . . . . . . . . 9 class (𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ)))
47 cnx 17125 . . . . . . . . . . 11 class ndx
48 cple 17203 . . . . . . . . . . 11 class le
4947, 48cfv 6543 . . . . . . . . . 10 class (leβ€˜ndx)
50 vg . . . . . . . . . . 11 setvar 𝑔
5134, 18cfv 6543 . . . . . . . . . . . 12 class (Baseβ€˜π‘‘)
52 vq . . . . . . . . . . . . . . . 16 setvar π‘ž
5352cv 1540 . . . . . . . . . . . . . . 15 class π‘ž
54 cdg1 25568 . . . . . . . . . . . . . . 15 class deg1
556, 53, 54co 7408 . . . . . . . . . . . . . 14 class (π‘Ÿ deg1 π‘ž)
566, 10, 54co 7408 . . . . . . . . . . . . . 14 class (π‘Ÿ deg1 𝑝)
57 clt 11247 . . . . . . . . . . . . . 14 class <
5855, 56, 57wbr 5148 . . . . . . . . . . . . 13 wff (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝)
5958, 52, 20crio 7363 . . . . . . . . . . . 12 class (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))
6017, 51, 59cmpt 5231 . . . . . . . . . . 11 class (𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝)))
6150cv 1540 . . . . . . . . . . . . 13 class 𝑔
6261ccnv 5675 . . . . . . . . . . . 12 class ◑𝑔
6312, 48cfv 6543 . . . . . . . . . . . . 13 class (leβ€˜π‘ )
6463, 61ccom 5680 . . . . . . . . . . . 12 class ((leβ€˜π‘ ) ∘ 𝑔)
6562, 64ccom 5680 . . . . . . . . . . 11 class (◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))
6650, 60, 65csb 3893 . . . . . . . . . 10 class ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))
6749, 66cop 4634 . . . . . . . . 9 class ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩
68 csts 17095 . . . . . . . . 9 class sSet
6946, 67, 68co 7408 . . . . . . . 8 class ((𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))) sSet ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩)
7031, 33, 69csb 3893 . . . . . . 7 class ⦋(𝑠 /s (𝑠 ~QG 𝑖)) / π‘‘β¦Œ((𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))) sSet ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩)
7170, 37cop 4634 . . . . . 6 class βŸ¨β¦‹(𝑠 /s (𝑠 ~QG 𝑖)) / π‘‘β¦Œ((𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))) sSet ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩), π‘“βŸ©
7216, 30, 71csb 3893 . . . . 5 class ⦋(𝑧 ∈ (Baseβ€˜π‘Ÿ) ↦ [(𝑧( ·𝑠 β€˜π‘ )(1rβ€˜π‘ ))](𝑠 ~QG 𝑖)) / π‘“β¦ŒβŸ¨β¦‹(𝑠 /s (𝑠 ~QG 𝑖)) / π‘‘β¦Œ((𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))) sSet ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩), π‘“βŸ©
739, 15, 72csb 3893 . . . 4 class ⦋((RSpanβ€˜π‘ )β€˜{𝑝}) / π‘–β¦Œβ¦‹(𝑧 ∈ (Baseβ€˜π‘Ÿ) ↦ [(𝑧( ·𝑠 β€˜π‘ )(1rβ€˜π‘ ))](𝑠 ~QG 𝑖)) / π‘“β¦ŒβŸ¨β¦‹(𝑠 /s (𝑠 ~QG 𝑖)) / π‘‘β¦Œ((𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))) sSet ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩), π‘“βŸ©
745, 8, 73csb 3893 . . 3 class ⦋(Poly1β€˜π‘Ÿ) / π‘ β¦Œβ¦‹((RSpanβ€˜π‘ )β€˜{𝑝}) / π‘–β¦Œβ¦‹(𝑧 ∈ (Baseβ€˜π‘Ÿ) ↦ [(𝑧( ·𝑠 β€˜π‘ )(1rβ€˜π‘ ))](𝑠 ~QG 𝑖)) / π‘“β¦ŒβŸ¨β¦‹(𝑠 /s (𝑠 ~QG 𝑖)) / π‘‘β¦Œ((𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))) sSet ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩), π‘“βŸ©
752, 3, 4, 4, 74cmpo 7410 . 2 class (π‘Ÿ ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1β€˜π‘Ÿ) / π‘ β¦Œβ¦‹((RSpanβ€˜π‘ )β€˜{𝑝}) / π‘–β¦Œβ¦‹(𝑧 ∈ (Baseβ€˜π‘Ÿ) ↦ [(𝑧( ·𝑠 β€˜π‘ )(1rβ€˜π‘ ))](𝑠 ~QG 𝑖)) / π‘“β¦ŒβŸ¨β¦‹(𝑠 /s (𝑠 ~QG 𝑖)) / π‘‘β¦Œ((𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))) sSet ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩), π‘“βŸ©)
761, 75wceq 1541 1 wff polyFld = (π‘Ÿ ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1β€˜π‘Ÿ) / π‘ β¦Œβ¦‹((RSpanβ€˜π‘ )β€˜{𝑝}) / π‘–β¦Œβ¦‹(𝑧 ∈ (Baseβ€˜π‘Ÿ) ↦ [(𝑧( ·𝑠 β€˜π‘ )(1rβ€˜π‘ ))](𝑠 ~QG 𝑖)) / π‘“β¦ŒβŸ¨β¦‹(𝑠 /s (𝑠 ~QG 𝑖)) / π‘‘β¦Œ((𝑑 toNrmGrp (℩𝑛 ∈ (AbsValβ€˜π‘‘)(𝑛 ∘ 𝑓) = (normβ€˜π‘Ÿ))) sSet ⟨(leβ€˜ndx), ⦋(𝑧 ∈ (Baseβ€˜π‘‘) ↦ (β„©π‘ž ∈ 𝑧 (π‘Ÿ deg1 π‘ž) < (π‘Ÿ deg1 𝑝))) / π‘”β¦Œ(◑𝑔 ∘ ((leβ€˜π‘ ) ∘ 𝑔))⟩), π‘“βŸ©)
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator