Mathbox for Steven Nguyen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  evlsval3 Structured version   Visualization version   GIF version

Theorem evlsval3 39770
 Description: Give a formula for the polynomial evaluation homomorphism. (Contributed by SN, 26-Jul-2024.)
Hypotheses
Ref Expression
evlsval3.q 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
evlsval3.p 𝑃 = (𝐼 mPoly 𝑈)
evlsval3.b 𝐵 = (Base‘𝑃)
evlsval3.d 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
evlsval3.k 𝐾 = (Base‘𝑆)
evlsval3.u 𝑈 = (𝑆s 𝑅)
evlsval3.t 𝑇 = (𝑆s (𝐾m 𝐼))
evlsval3.m 𝑀 = (mulGrp‘𝑇)
evlsval3.w = (.g𝑀)
evlsval3.x · = (.r𝑇)
evlsval3.e 𝐸 = (𝑝𝐵 ↦ (𝑇 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑀 Σg (𝑏f 𝐺))))))
evlsval3.f 𝐹 = (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))
evlsval3.g 𝐺 = (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))
evlsval3.i (𝜑𝐼𝑉)
evlsval3.s (𝜑𝑆 ∈ CRing)
evlsval3.r (𝜑𝑅 ∈ (SubRing‘𝑆))
Assertion
Ref Expression
evlsval3 (𝜑𝑄 = 𝐸)
Distinct variable groups:   𝜑,𝑎,𝑥   𝜑,𝑏,𝑝   𝑃,𝑏,𝑝   𝐵,𝑏,𝑝   𝐷,𝑏,𝑝   𝐾,𝑎,𝑥   𝑈,𝑏,,𝑝   𝑇,𝑏,𝑝   𝑥,𝑇   𝑀,𝑏,𝑝   ,𝑏,𝑝   · ,𝑏,𝑝   𝐹,𝑏,𝑝   𝐺,𝑏,𝑝   𝐼,𝑎,𝑥   𝐼,𝑏,,𝑝   𝑆,𝑎,𝑥   𝑥,𝑅
Allowed substitution hints:   𝜑()   𝐵(𝑥,,𝑎)   𝐷(𝑥,,𝑎)   𝑃(𝑥,,𝑎)   𝑄(𝑥,,𝑝,𝑎,𝑏)   𝑅(,𝑝,𝑎,𝑏)   𝑆(,𝑝,𝑏)   𝑇(,𝑎)   · (𝑥,,𝑎)   𝑈(𝑥,𝑎)   𝐸(𝑥,,𝑝,𝑎,𝑏)   (𝑥,,𝑎)   𝐹(𝑥,,𝑎)   𝐺(𝑥,,𝑎)   𝐾(,𝑝,𝑏)   𝑀(𝑥,,𝑎)   𝑉(𝑥,,𝑝,𝑎,𝑏)

Proof of Theorem evlsval3
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 evlsval3.i . . 3 (𝜑𝐼𝑉)
2 evlsval3.s . . 3 (𝜑𝑆 ∈ CRing)
3 evlsval3.r . . 3 (𝜑𝑅 ∈ (SubRing‘𝑆))
4 evlsval3.q . . . 4 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
5 evlsval3.p . . . 4 𝑃 = (𝐼 mPoly 𝑈)
6 eqid 2759 . . . 4 (𝐼 mVar 𝑈) = (𝐼 mVar 𝑈)
7 evlsval3.u . . . 4 𝑈 = (𝑆s 𝑅)
8 evlsval3.t . . . 4 𝑇 = (𝑆s (𝐾m 𝐼))
9 evlsval3.k . . . 4 𝐾 = (Base‘𝑆)
10 eqid 2759 . . . 4 (algSc‘𝑃) = (algSc‘𝑃)
11 evlsval3.f . . . 4 𝐹 = (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥}))
12 evlsval3.g . . . 4 𝐺 = (𝑥𝐼 ↦ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)))
134, 5, 6, 7, 8, 9, 10, 11, 12evlsval 20842 . . 3 ((𝐼𝑉𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (𝑓 ∈ (𝑃 RingHom 𝑇)((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺)))
141, 2, 3, 13syl3anc 1369 . 2 (𝜑𝑄 = (𝑓 ∈ (𝑃 RingHom 𝑇)((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺)))
15 evlsval3.b . . . . 5 𝐵 = (Base‘𝑃)
16 eqid 2759 . . . . 5 (Base‘𝑇) = (Base‘𝑇)
17 evlsval3.d . . . . 5 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
18 evlsval3.m . . . . 5 𝑀 = (mulGrp‘𝑇)
19 evlsval3.w . . . . 5 = (.g𝑀)
20 evlsval3.x . . . . 5 · = (.r𝑇)
21 evlsval3.e . . . . 5 𝐸 = (𝑝𝐵 ↦ (𝑇 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑀 Σg (𝑏f 𝐺))))))
227subrgcrng 19600 . . . . . 6 ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing)
232, 3, 22syl2anc 588 . . . . 5 (𝜑𝑈 ∈ CRing)
24 ovexd 7186 . . . . . 6 (𝜑 → (𝐾m 𝐼) ∈ V)
258pwscrng 19431 . . . . . 6 ((𝑆 ∈ CRing ∧ (𝐾m 𝐼) ∈ V) → 𝑇 ∈ CRing)
262, 24, 25syl2anc 588 . . . . 5 (𝜑𝑇 ∈ CRing)
279subrgss 19597 . . . . . . . . 9 (𝑅 ∈ (SubRing‘𝑆) → 𝑅𝐾)
283, 27syl 17 . . . . . . . 8 (𝜑𝑅𝐾)
2928resmptd 5881 . . . . . . 7 (𝜑 → ((𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥})) ↾ 𝑅) = (𝑥𝑅 ↦ ((𝐾m 𝐼) × {𝑥})))
3011, 29eqtr4id 2813 . . . . . 6 (𝜑𝐹 = ((𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥})) ↾ 𝑅))
312crngringd 19371 . . . . . . . 8 (𝜑𝑆 ∈ Ring)
32 eqid 2759 . . . . . . . . 9 (𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥})) = (𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥}))
338, 9, 32pwsdiagrhm 19630 . . . . . . . 8 ((𝑆 ∈ Ring ∧ (𝐾m 𝐼) ∈ V) → (𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇))
3431, 24, 33syl2anc 588 . . . . . . 7 (𝜑 → (𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇))
357resrhm 19625 . . . . . . 7 (((𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇) ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥})) ↾ 𝑅) ∈ (𝑈 RingHom 𝑇))
3634, 3, 35syl2anc 588 . . . . . 6 (𝜑 → ((𝑥𝐾 ↦ ((𝐾m 𝐼) × {𝑥})) ↾ 𝑅) ∈ (𝑈 RingHom 𝑇))
3730, 36eqeltrd 2853 . . . . 5 (𝜑𝐹 ∈ (𝑈 RingHom 𝑇))
389fvexi 6673 . . . . . . . . . . . 12 𝐾 ∈ V
39 elmapg 8430 . . . . . . . . . . . 12 ((𝐾 ∈ V ∧ 𝐼𝑉) → (𝑎 ∈ (𝐾m 𝐼) ↔ 𝑎:𝐼𝐾))
4038, 1, 39sylancr 591 . . . . . . . . . . 11 (𝜑 → (𝑎 ∈ (𝐾m 𝐼) ↔ 𝑎:𝐼𝐾))
4140biimpa 481 . . . . . . . . . 10 ((𝜑𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
4241adantlr 715 . . . . . . . . 9 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑎:𝐼𝐾)
43 simplr 769 . . . . . . . . 9 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → 𝑥𝐼)
4442, 43ffvelrnd 6844 . . . . . . . 8 (((𝜑𝑥𝐼) ∧ 𝑎 ∈ (𝐾m 𝐼)) → (𝑎𝑥) ∈ 𝐾)
4544fmpttd 6871 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾)
46 ovexd 7186 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝐾m 𝐼) ∈ V)
478, 9, 16pwselbasb 16812 . . . . . . . 8 ((𝑆 ∈ CRing ∧ (𝐾m 𝐼) ∈ V) → ((𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘𝑇) ↔ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾))
482, 46, 47syl2an2r 685 . . . . . . 7 ((𝜑𝑥𝐼) → ((𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘𝑇) ↔ (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)):(𝐾m 𝐼)⟶𝐾))
4945, 48mpbird 260 . . . . . 6 ((𝜑𝑥𝐼) → (𝑎 ∈ (𝐾m 𝐼) ↦ (𝑎𝑥)) ∈ (Base‘𝑇))
5049, 12fmptd 6870 . . . . 5 (𝜑𝐺:𝐼⟶(Base‘𝑇))
515, 15, 16, 17, 18, 19, 20, 6, 21, 1, 23, 26, 37, 50, 10evlslem1 20838 . . . 4 (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑇) ∧ (𝐸 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝐸 ∘ (𝐼 mVar 𝑈)) = 𝐺))
5251simp2d 1141 . . 3 (𝜑 → (𝐸 ∘ (algSc‘𝑃)) = 𝐹)
5351simp3d 1142 . . 3 (𝜑 → (𝐸 ∘ (𝐼 mVar 𝑈)) = 𝐺)
5451simp1d 1140 . . . 4 (𝜑𝐸 ∈ (𝑃 RingHom 𝑇))
555, 16, 10, 6, 1, 23, 26, 37, 50evlseu 20839 . . . 4 (𝜑 → ∃!𝑓 ∈ (𝑃 RingHom 𝑇)((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺))
56 coeq1 5698 . . . . . . 7 (𝑓 = 𝐸 → (𝑓 ∘ (algSc‘𝑃)) = (𝐸 ∘ (algSc‘𝑃)))
5756eqeq1d 2761 . . . . . 6 (𝑓 = 𝐸 → ((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ↔ (𝐸 ∘ (algSc‘𝑃)) = 𝐹))
58 coeq1 5698 . . . . . . 7 (𝑓 = 𝐸 → (𝑓 ∘ (𝐼 mVar 𝑈)) = (𝐸 ∘ (𝐼 mVar 𝑈)))
5958eqeq1d 2761 . . . . . 6 (𝑓 = 𝐸 → ((𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺 ↔ (𝐸 ∘ (𝐼 mVar 𝑈)) = 𝐺))
6057, 59anbi12d 634 . . . . 5 (𝑓 = 𝐸 → (((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺) ↔ ((𝐸 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝐸 ∘ (𝐼 mVar 𝑈)) = 𝐺)))
6160riota2 7134 . . . 4 ((𝐸 ∈ (𝑃 RingHom 𝑇) ∧ ∃!𝑓 ∈ (𝑃 RingHom 𝑇)((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺)) → (((𝐸 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝐸 ∘ (𝐼 mVar 𝑈)) = 𝐺) ↔ (𝑓 ∈ (𝑃 RingHom 𝑇)((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺)) = 𝐸))
6254, 55, 61syl2anc 588 . . 3 (𝜑 → (((𝐸 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝐸 ∘ (𝐼 mVar 𝑈)) = 𝐺) ↔ (𝑓 ∈ (𝑃 RingHom 𝑇)((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺)) = 𝐸))
6352, 53, 62mpbi2and 712 . 2 (𝜑 → (𝑓 ∈ (𝑃 RingHom 𝑇)((𝑓 ∘ (algSc‘𝑃)) = 𝐹 ∧ (𝑓 ∘ (𝐼 mVar 𝑈)) = 𝐺)) = 𝐸)
6414, 63eqtrd 2794 1 (𝜑𝑄 = 𝐸)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∃!wreu 3073  {crab 3075  Vcvv 3410   ⊆ wss 3859  {csn 4523   ↦ cmpt 5113   × cxp 5523  ◡ccnv 5524   ↾ cres 5527   “ cima 5528   ∘ ccom 5529  ⟶wf 6332  ‘cfv 6336  ℩crio 7108  (class class class)co 7151   ∘f cof 7404   ↑m cmap 8417  Fincfn 8528  ℕcn 11667  ℕ0cn0 11927  Basecbs 16534   ↾s cress 16535  .rcmulr 16617   Σg cgsu 16765   ↑s cpws 16771  .gcmg 18284  mulGrpcmgp 19300  Ringcrg 19358  CRingccrg 19359   RingHom crh 19528  SubRingcsubrg 19592  algSccascl 20610   mVar cmvr 20660   mPoly cmpl 20661   evalSub ces 20826 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10624  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7406  df-ofr 7407  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-2o 8114  df-oadd 8117  df-er 8300  df-map 8419  df-pm 8420  df-ixp 8481  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-fsupp 8860  df-sup 8932  df-oi 9000  df-card 9394  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-nn 11668  df-2 11730  df-3 11731  df-4 11732  df-5 11733  df-6 11734  df-7 11735  df-8 11736  df-9 11737  df-n0 11928  df-z 12014  df-dec 12131  df-uz 12276  df-fz 12933  df-fzo 13076  df-seq 13412  df-hash 13734  df-struct 16536  df-ndx 16537  df-slot 16538  df-base 16540  df-sets 16541  df-ress 16542  df-plusg 16629  df-mulr 16630  df-sca 16632  df-vsca 16633  df-ip 16634  df-tset 16635  df-ple 16636  df-ds 16638  df-hom 16640  df-cco 16641  df-0g 16766  df-gsum 16767  df-prds 16772  df-pws 16774  df-mre 16908  df-mrc 16909  df-acs 16911  df-mgm 17911  df-sgrp 17960  df-mnd 17971  df-mhm 18015  df-submnd 18016  df-grp 18165  df-minusg 18166  df-sbg 18167  df-mulg 18285  df-subg 18336  df-ghm 18416  df-cntz 18507  df-cmn 18968  df-abl 18969  df-mgp 19301  df-ur 19313  df-srg 19317  df-ring 19360  df-cring 19361  df-rnghom 19531  df-subrg 19594  df-lmod 19697  df-lss 19765  df-lsp 19805  df-assa 20611  df-asp 20612  df-ascl 20613  df-psr 20664  df-mvr 20665  df-mpl 20666  df-evls 20828 This theorem is referenced by:  evlsbagval  39773
 Copyright terms: Public domain W3C validator