Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  algnbval Structured version   Visualization version   GIF version

Theorem algnbval 32174
Description: The algebraic numbers over a field 𝐹 within a field 𝐸. That is, the numbers 𝑋 which are roots of nonzero polynomials 𝑝(𝑋) with coefficients in (Base‘𝐹). This is expressed by the idiom ((𝑂𝑝) “ { 0 }), which can be translated into {𝑥 ∈ (Base‘𝐸) ∣ ((𝑂𝑝)‘𝑥) = 0 } by fniniseg2 7009. (Contributed by Thierry Arnoux, 26-Jan-2025.)
Hypotheses
Ref Expression
algnbval.o 𝑂 = (𝐸 evalSub1 𝐹)
algnbval.z 𝑍 = (0g‘(Poly1𝐸))
algnbval.1 0 = (0g𝐸)
algnbval.2 (𝜑𝐸 ∈ Field)
algnbval.3 (𝜑𝐹 ∈ (SubDRing‘𝐸))
Assertion
Ref Expression
algnbval (𝜑 → (𝐸 AlgNb 𝐹) = 𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }))
Distinct variable groups:   𝐸,𝑝   𝐹,𝑝   𝑂,𝑝   𝑍,𝑝
Allowed substitution hints:   𝜑(𝑝)   0 (𝑝)

Proof of Theorem algnbval
Dummy variables 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 algnbval.2 . . 3 (𝜑𝐸 ∈ Field)
21elexd 3463 . 2 (𝜑𝐸 ∈ V)
3 algnbval.3 . . 3 (𝜑𝐹 ∈ (SubDRing‘𝐸))
43elexd 3463 . 2 (𝜑𝐹 ∈ V)
5 algnbval.o . . . . . . 7 𝑂 = (𝐸 evalSub1 𝐹)
65ovexi 7385 . . . . . 6 𝑂 ∈ V
76dmex 7840 . . . . 5 dom 𝑂 ∈ V
87difexi 5283 . . . 4 (dom 𝑂 ∖ {𝑍}) ∈ V
98a1i 11 . . 3 (𝜑 → (dom 𝑂 ∖ {𝑍}) ∈ V)
10 fvex 6852 . . . . . 6 (𝑂𝑝) ∈ V
1110cnvex 7854 . . . . 5 (𝑂𝑝) ∈ V
1211imaex 7845 . . . 4 ((𝑂𝑝) “ { 0 }) ∈ V
1312rgenw 3066 . . 3 𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }) ∈ V
14 iunexg 7888 . . 3 (((dom 𝑂 ∖ {𝑍}) ∈ V ∧ ∀𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }) ∈ V) → 𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }) ∈ V)
159, 13, 14sylancl 586 . 2 (𝜑 𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }) ∈ V)
16 oveq12 7360 . . . . . . 7 ((𝑒 = 𝐸𝑓 = 𝐹) → (𝑒 evalSub1 𝑓) = (𝐸 evalSub1 𝐹))
1716, 5eqtr4di 2795 . . . . . 6 ((𝑒 = 𝐸𝑓 = 𝐹) → (𝑒 evalSub1 𝑓) = 𝑂)
1817dmeqd 5859 . . . . 5 ((𝑒 = 𝐸𝑓 = 𝐹) → dom (𝑒 evalSub1 𝑓) = dom 𝑂)
19 simpl 483 . . . . . . . . 9 ((𝑒 = 𝐸𝑓 = 𝐹) → 𝑒 = 𝐸)
2019fveq2d 6843 . . . . . . . 8 ((𝑒 = 𝐸𝑓 = 𝐹) → (Poly1𝑒) = (Poly1𝐸))
2120fveq2d 6843 . . . . . . 7 ((𝑒 = 𝐸𝑓 = 𝐹) → (0g‘(Poly1𝑒)) = (0g‘(Poly1𝐸)))
22 algnbval.z . . . . . . 7 𝑍 = (0g‘(Poly1𝐸))
2321, 22eqtr4di 2795 . . . . . 6 ((𝑒 = 𝐸𝑓 = 𝐹) → (0g‘(Poly1𝑒)) = 𝑍)
2423sneqd 4596 . . . . 5 ((𝑒 = 𝐸𝑓 = 𝐹) → {(0g‘(Poly1𝑒))} = {𝑍})
2518, 24difeq12d 4081 . . . 4 ((𝑒 = 𝐸𝑓 = 𝐹) → (dom (𝑒 evalSub1 𝑓) ∖ {(0g‘(Poly1𝑒))}) = (dom 𝑂 ∖ {𝑍}))
2617fveq1d 6841 . . . . . 6 ((𝑒 = 𝐸𝑓 = 𝐹) → ((𝑒 evalSub1 𝑓)‘𝑝) = (𝑂𝑝))
2726cnveqd 5829 . . . . 5 ((𝑒 = 𝐸𝑓 = 𝐹) → ((𝑒 evalSub1 𝑓)‘𝑝) = (𝑂𝑝))
2819fveq2d 6843 . . . . . . 7 ((𝑒 = 𝐸𝑓 = 𝐹) → (0g𝑒) = (0g𝐸))
29 algnbval.1 . . . . . . 7 0 = (0g𝐸)
3028, 29eqtr4di 2795 . . . . . 6 ((𝑒 = 𝐸𝑓 = 𝐹) → (0g𝑒) = 0 )
3130sneqd 4596 . . . . 5 ((𝑒 = 𝐸𝑓 = 𝐹) → {(0g𝑒)} = { 0 })
3227, 31imaeq12d 6012 . . . 4 ((𝑒 = 𝐸𝑓 = 𝐹) → (((𝑒 evalSub1 𝑓)‘𝑝) “ {(0g𝑒)}) = ((𝑂𝑝) “ { 0 }))
3325, 32iuneq12d 4980 . . 3 ((𝑒 = 𝐸𝑓 = 𝐹) → 𝑝 ∈ (dom (𝑒 evalSub1 𝑓) ∖ {(0g‘(Poly1𝑒))})(((𝑒 evalSub1 𝑓)‘𝑝) “ {(0g𝑒)}) = 𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }))
34 df-algnb 32172 . . 3 AlgNb = (𝑒 ∈ V, 𝑓 ∈ V ↦ 𝑝 ∈ (dom (𝑒 evalSub1 𝑓) ∖ {(0g‘(Poly1𝑒))})(((𝑒 evalSub1 𝑓)‘𝑝) “ {(0g𝑒)}))
3533, 34ovmpoga 7503 . 2 ((𝐸 ∈ V ∧ 𝐹 ∈ V ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }) ∈ V) → (𝐸 AlgNb 𝐹) = 𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }))
362, 4, 15, 35syl3anc 1371 1 (𝜑 → (𝐸 AlgNb 𝐹) = 𝑝 ∈ (dom 𝑂 ∖ {𝑍})((𝑂𝑝) “ { 0 }))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wral 3062  Vcvv 3443  cdif 3905  {csn 4584   ciun 4952  ccnv 5630  dom cdm 5631  cima 5634  cfv 6493  (class class class)co 7351  0gc0g 17280  Fieldcfield 20138  SubDRingcsdrg 20211  Poly1cpl1 21499   evalSub1 ces1 21630   AlgNb calgnb 32170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6445  df-fun 6495  df-fv 6501  df-ov 7354  df-oprab 7355  df-mpo 7356  df-algnb 32172
This theorem is referenced by:  isalgnb  32175
  Copyright terms: Public domain W3C validator