Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > evl1rhm | Structured version Visualization version GIF version |
Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Mario Carneiro, 12-Jun-2015.) (Proof shortened by AV, 13-Sep-2019.) |
Ref | Expression |
---|---|
evl1rhm.q | ⊢ 𝑂 = (eval1‘𝑅) |
evl1rhm.w | ⊢ 𝑃 = (Poly1‘𝑅) |
evl1rhm.t | ⊢ 𝑇 = (𝑅 ↑s 𝐵) |
evl1rhm.b | ⊢ 𝐵 = (Base‘𝑅) |
Ref | Expression |
---|---|
evl1rhm | ⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom 𝑇)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evl1rhm.q | . . 3 ⊢ 𝑂 = (eval1‘𝑅) | |
2 | eqid 2739 | . . 3 ⊢ (1o eval 𝑅) = (1o eval 𝑅) | |
3 | evl1rhm.b | . . 3 ⊢ 𝐵 = (Base‘𝑅) | |
4 | 1, 2, 3 | evl1fval 21503 | . 2 ⊢ 𝑂 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (1o eval 𝑅)) |
5 | evl1rhm.t | . . . 4 ⊢ 𝑇 = (𝑅 ↑s 𝐵) | |
6 | eqid 2739 | . . . 4 ⊢ (𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) = (𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) | |
7 | 3, 5, 6 | evls1rhmlem 21496 | . . 3 ⊢ (𝑅 ∈ CRing → (𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∈ ((𝑅 ↑s (𝐵 ↑m 1o)) RingHom 𝑇)) |
8 | 1on 8318 | . . . . 5 ⊢ 1o ∈ On | |
9 | eqid 2739 | . . . . . 6 ⊢ (1o mPoly 𝑅) = (1o mPoly 𝑅) | |
10 | eqid 2739 | . . . . . 6 ⊢ (𝑅 ↑s (𝐵 ↑m 1o)) = (𝑅 ↑s (𝐵 ↑m 1o)) | |
11 | 2, 3, 9, 10 | evlrhm 21315 | . . . . 5 ⊢ ((1o ∈ On ∧ 𝑅 ∈ CRing) → (1o eval 𝑅) ∈ ((1o mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑m 1o)))) |
12 | 8, 11 | mpan 687 | . . . 4 ⊢ (𝑅 ∈ CRing → (1o eval 𝑅) ∈ ((1o mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑m 1o)))) |
13 | eqidd 2740 | . . . . 5 ⊢ (𝑅 ∈ CRing → (Base‘𝑃) = (Base‘𝑃)) | |
14 | eqidd 2740 | . . . . 5 ⊢ (𝑅 ∈ CRing → (Base‘(𝑅 ↑s (𝐵 ↑m 1o))) = (Base‘(𝑅 ↑s (𝐵 ↑m 1o)))) | |
15 | evl1rhm.w | . . . . . . 7 ⊢ 𝑃 = (Poly1‘𝑅) | |
16 | eqid 2739 | . . . . . . 7 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅) | |
17 | eqid 2739 | . . . . . . 7 ⊢ (Base‘𝑃) = (Base‘𝑃) | |
18 | 15, 16, 17 | ply1bas 21375 | . . . . . 6 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅)) |
19 | 18 | a1i 11 | . . . . 5 ⊢ (𝑅 ∈ CRing → (Base‘𝑃) = (Base‘(1o mPoly 𝑅))) |
20 | eqid 2739 | . . . . . . . 8 ⊢ (+g‘𝑃) = (+g‘𝑃) | |
21 | 15, 9, 20 | ply1plusg 21405 | . . . . . . 7 ⊢ (+g‘𝑃) = (+g‘(1o mPoly 𝑅)) |
22 | 21 | a1i 11 | . . . . . 6 ⊢ (𝑅 ∈ CRing → (+g‘𝑃) = (+g‘(1o mPoly 𝑅))) |
23 | 22 | oveqdr 7312 | . . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → (𝑥(+g‘𝑃)𝑦) = (𝑥(+g‘(1o mPoly 𝑅))𝑦)) |
24 | eqidd 2740 | . . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑥 ∈ (Base‘(𝑅 ↑s (𝐵 ↑m 1o))) ∧ 𝑦 ∈ (Base‘(𝑅 ↑s (𝐵 ↑m 1o))))) → (𝑥(+g‘(𝑅 ↑s (𝐵 ↑m 1o)))𝑦) = (𝑥(+g‘(𝑅 ↑s (𝐵 ↑m 1o)))𝑦)) | |
25 | eqid 2739 | . . . . . . . 8 ⊢ (.r‘𝑃) = (.r‘𝑃) | |
26 | 15, 9, 25 | ply1mulr 21407 | . . . . . . 7 ⊢ (.r‘𝑃) = (.r‘(1o mPoly 𝑅)) |
27 | 26 | a1i 11 | . . . . . 6 ⊢ (𝑅 ∈ CRing → (.r‘𝑃) = (.r‘(1o mPoly 𝑅))) |
28 | 27 | oveqdr 7312 | . . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → (𝑥(.r‘𝑃)𝑦) = (𝑥(.r‘(1o mPoly 𝑅))𝑦)) |
29 | eqidd 2740 | . . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑥 ∈ (Base‘(𝑅 ↑s (𝐵 ↑m 1o))) ∧ 𝑦 ∈ (Base‘(𝑅 ↑s (𝐵 ↑m 1o))))) → (𝑥(.r‘(𝑅 ↑s (𝐵 ↑m 1o)))𝑦) = (𝑥(.r‘(𝑅 ↑s (𝐵 ↑m 1o)))𝑦)) | |
30 | 13, 14, 19, 14, 23, 24, 28, 29 | rhmpropd 20069 | . . . 4 ⊢ (𝑅 ∈ CRing → (𝑃 RingHom (𝑅 ↑s (𝐵 ↑m 1o))) = ((1o mPoly 𝑅) RingHom (𝑅 ↑s (𝐵 ↑m 1o)))) |
31 | 12, 30 | eleqtrrd 2843 | . . 3 ⊢ (𝑅 ∈ CRing → (1o eval 𝑅) ∈ (𝑃 RingHom (𝑅 ↑s (𝐵 ↑m 1o)))) |
32 | rhmco 19990 | . . 3 ⊢ (((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∈ ((𝑅 ↑s (𝐵 ↑m 1o)) RingHom 𝑇) ∧ (1o eval 𝑅) ∈ (𝑃 RingHom (𝑅 ↑s (𝐵 ↑m 1o)))) → ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (1o eval 𝑅)) ∈ (𝑃 RingHom 𝑇)) | |
33 | 7, 31, 32 | syl2anc 584 | . 2 ⊢ (𝑅 ∈ CRing → ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (1o eval 𝑅)) ∈ (𝑃 RingHom 𝑇)) |
34 | 4, 33 | eqeltrid 2844 | 1 ⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom 𝑇)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1539 ∈ wcel 2107 {csn 4562 ↦ cmpt 5158 × cxp 5588 ∘ ccom 5594 Oncon0 6270 ‘cfv 6437 (class class class)co 7284 1oc1o 8299 ↑m cmap 8624 Basecbs 16921 +gcplusg 16971 .rcmulr 16972 ↑s cpws 17166 CRingccrg 19793 RingHom crh 19965 mPoly cmpl 21118 eval cevl 21290 PwSer1cps1 21355 Poly1cpl1 21357 eval1ce1 21489 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-iin 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-se 5546 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-isom 6446 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-of 7542 df-ofr 7543 df-om 7722 df-1st 7840 df-2nd 7841 df-supp 7987 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-er 8507 df-map 8626 df-pm 8627 df-ixp 8695 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-fsupp 9138 df-sup 9210 df-oi 9278 df-card 9706 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-nn 11983 df-2 12045 df-3 12046 df-4 12047 df-5 12048 df-6 12049 df-7 12050 df-8 12051 df-9 12052 df-n0 12243 df-z 12329 df-dec 12447 df-uz 12592 df-fz 13249 df-fzo 13392 df-seq 13731 df-hash 14054 df-struct 16857 df-sets 16874 df-slot 16892 df-ndx 16904 df-base 16922 df-ress 16951 df-plusg 16984 df-mulr 16985 df-sca 16987 df-vsca 16988 df-ip 16989 df-tset 16990 df-ple 16991 df-ds 16993 df-hom 16995 df-cco 16996 df-0g 17161 df-gsum 17162 df-prds 17167 df-pws 17169 df-mre 17304 df-mrc 17305 df-acs 17307 df-mgm 18335 df-sgrp 18384 df-mnd 18395 df-mhm 18439 df-submnd 18440 df-grp 18589 df-minusg 18590 df-sbg 18591 df-mulg 18710 df-subg 18761 df-ghm 18841 df-cntz 18932 df-cmn 19397 df-abl 19398 df-mgp 19730 df-ur 19747 df-srg 19751 df-ring 19794 df-cring 19795 df-rnghom 19968 df-subrg 20031 df-lmod 20134 df-lss 20203 df-lsp 20243 df-assa 21069 df-asp 21070 df-ascl 21071 df-psr 21121 df-mvr 21122 df-mpl 21123 df-opsr 21125 df-evls 21291 df-evl 21292 df-psr1 21360 df-ply1 21362 df-evl1 21491 |
This theorem is referenced by: fveval1fvcl 21508 evl1addd 21516 evl1subd 21517 evl1muld 21518 evl1expd 21520 pf1const 21521 pf1id 21522 pf1subrg 21523 mpfpf1 21526 pf1mpf 21527 evl1gsummul 21535 evl1scvarpw 21538 ply1remlem 25336 ply1rem 25337 fta1glem1 25339 fta1glem2 25340 fta1g 25341 fta1blem 25342 plypf1 25382 lgsqrlem2 26504 lgsqrlem3 26505 pl1cn 31914 idomrootle 41027 |
Copyright terms: Public domain | W3C validator |