evlsgsumadd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > evlsgsumadd		Structured version Visualization version GIF version

Theorem evlsgsumadd 22417

Description: Polynomial evaluation maps (additive) group sums to group sums. (Contributed by SN, 13-Feb-2024.)

**Hypotheses**
Ref	Expression
evlsgsumadd.q	⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
evlsgsumadd.w	⊢ 𝑊 = (𝐼 mPoly 𝑈)
evlsgsumadd.0	⊢ 0 = (0_g‘𝑊)
evlsgsumadd.u	⊢ 𝑈 = (𝑆 ↾_s 𝑅)
evlsgsumadd.p	⊢ 𝑃 = (𝑆 ↑_s (𝐾 ↑_m 𝐼))
evlsgsumadd.k	⊢ 𝐾 = (Base‘𝑆)
evlsgsumadd.b	⊢ 𝐵 = (Base‘𝑊)
evlsgsumadd.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
evlsgsumadd.s	⊢ (𝜑 → 𝑆 ∈ CRing)
evlsgsumadd.r	⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
evlsgsumadd.y	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)
evlsgsumadd.n	⊢ (𝜑 → 𝑁 ⊆ ℕ₀)
evlsgsumadd.f	⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )

**Assertion**
Ref	Expression
evlsgsumadd	⊢ (𝜑 → (𝑄‘(𝑊 Σ_g (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σ_g (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))

Distinct variable groups: 𝑥,𝐵 𝑥,𝑁 𝑥,𝑄 𝜑,𝑥 Allowed substitution hints: 𝑃(𝑥) 𝑅(𝑥) 𝑆(𝑥) 𝑈(𝑥) 𝐼(𝑥) 𝐾(𝑥) 𝑉(𝑥) 𝑊(𝑥) 𝑌(𝑥) 0 (𝑥)

**Proof of Theorem evlsgsumadd**
Step	Hyp	Ref	Expression
1		evlsgsumadd.b	. . 3 ⊢ 𝐵 = (Base‘𝑊)
2		evlsgsumadd.0	. . 3 ⊢ 0 = (0_g‘𝑊)
3		evlsgsumadd.w	. . . . 5 ⊢ 𝑊 = (𝐼 mPoly 𝑈)
4		evlsgsumadd.i	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
5		evlsgsumadd.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
6		evlsgsumadd.u	. . . . . . 7 ⊢ 𝑈 = (𝑆 ↾_s 𝑅)
7	6	subrgring 20838	. . . . . 6 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
8	5, 7	syl 18	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ Ring)
9	3, 4, 8	mplringd 22342	. . . 4 ⊢ (𝜑 → 𝑊 ∈ Ring)
10		ringcmn 20523	. . . 4 ⊢ (𝑊 ∈ Ring → 𝑊 ∈ CMnd)
11	9, 10	syl 18	. . 3 ⊢ (𝜑 → 𝑊 ∈ CMnd)
12		evlsgsumadd.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ CRing)
13		crngring 20484	. . . . . 6 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
14	12, 13	syl 18	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Ring)
15		ovex 7460	. . . . 5 ⊢ (𝐾 ↑_m 𝐼) ∈ V
16	14, 15	jctir 530	. . . 4 ⊢ (𝜑 → (𝑆 ∈ Ring ∧ (𝐾 ↑_m 𝐼) ∈ V))
17		evlsgsumadd.p	. . . . 5 ⊢ 𝑃 = (𝑆 ↑_s (𝐾 ↑_m 𝐼))
18	17	pwsring 20565	. . . 4 ⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑_m 𝐼) ∈ V) → 𝑃 ∈ Ring)
19		ringmnd 20482	. . . 4 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
20	16, 18, 19	3syl 19	. . 3 ⊢ (𝜑 → 𝑃 ∈ Mnd)
21		nn0ex 12622	. . . . 5 ⊢ ℕ₀ ∈ V
22	21	a1i 11	. . . 4 ⊢ (𝜑 → ℕ₀ ∈ V)
23		evlsgsumadd.n	. . . 4 ⊢ (𝜑 → 𝑁 ⊆ ℕ₀)
24	22, 23	ssexd 5289	. . 3 ⊢ (𝜑 → 𝑁 ∈ V)
25		evlsgsumadd.q	. . . . . 6 ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
26		evlsgsumadd.k	. . . . . 6 ⊢ 𝐾 = (Base‘𝑆)
27	25, 3, 6, 17, 26	evlsrhm 22409	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom 𝑃))
28	4, 12, 5, 27	syl3anc 1398	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom 𝑃))
29		rhmghm 20726	. . . 4 ⊢ (𝑄 ∈ (𝑊 RingHom 𝑃) → 𝑄 ∈ (𝑊 GrpHom 𝑃))
30		ghmmhm 19452	. . . 4 ⊢ (𝑄 ∈ (𝑊 GrpHom 𝑃) → 𝑄 ∈ (𝑊 MndHom 𝑃))
31	28, 29, 30	3syl 19	. . 3 ⊢ (𝜑 → 𝑄 ∈ (𝑊 MndHom 𝑃))
32		evlsgsumadd.y	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)
33		evlsgsumadd.f	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )
34	1, 2, 11, 20, 24, 31, 32, 33	gsummptmhm 20166	. 2 ⊢ (𝜑 → (𝑃 Σ_g (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))) = (𝑄‘(𝑊 Σ_g (𝑥 ∈ 𝑁 ↦ 𝑌))))
35	34	eqcomd 2769	1 ⊢ (𝜑 → (𝑄‘(𝑊 Σ_g (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σ_g (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2146 Vcvv 3453 ⊆ wss 3899 class class class wbr 5105 ↦ cmpt 5188 ‘cfv 6546 (class class class)co 7427 ↑_m cmap 8858 finSupp cfsupp 9364 ℕ₀cn0 12616 Basecbs 17399 ↾_s cress 17420 0_gc0g 17622 Σ_g cgsu 17623 ↑_s cpws 17629 Mndcmnd 18935 MndHom cmhm 18988 GrpHom cghm 19439 CMndccmn 20006 Ringcrg 20471 CRingccrg 20472 RingHom crh 20711 SubRingcsubrg 20833 mPoly cmpl 22226 evalSub ces 22393

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4838 df-uni 4870 df-int 4910 df-iun 4955 df-iin 4956 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-se 5608 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-isom 6555 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-of 7700 df-ofr 7701 df-om 7885 df-1st 8008 df-2nd 8009 df-supp 8188 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-1o 8487 df-2o 8488 df-er 8728 df-map 8860 df-pm 8861 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9365 df-sup 9444 df-oi 9514 df-card 10030 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-nn 12346 df-2 12415 df-3 12416 df-4 12417 df-5 12418 df-6 12419 df-7 12420 df-8 12421 df-9 12422 df-n0 12617 df-z 12704 df-dec 12825 df-uz 12976 df-fz 13650 df-fzo 13799 df-seq 14155 df-hash 14485 df-struct 17337 df-sets 17354 df-slot 17372 df-ndx 17384 df-base 17400 df-ress 17421 df-plusg 17453 df-mulr 17454 df-sca 17456 df-vsca 17457 df-ip 17458 df-tset 17459 df-ple 17460 df-ds 17462 df-hom 17464 df-cco 17465 df-0g 17624 df-gsum 17625 df-prds 17630 df-pws 17632 df-mre 17768 df-mrc 17769 df-acs 17771 df-mgm 18828 df-sgrp 18920 df-mnd 18936 df-mhm 18990 df-submnd 18991 df-grp 19159 df-minusg 19160 df-sbg 19161 df-mulg 19290 df-subg 19345 df-ghm 19440 df-cntz 19543 df-cmn 20008 df-abl 20009 df-mgp 20373 df-rng 20387 df-ur 20420 df-srg 20425 df-ring 20473 df-cring 20474 df-rhm 20714 df-subrng 20810 df-subrg 20834 df-lmod 21149 df-lss 21219 df-lsp 21259 df-assa 22173 df-asp 22174 df-ascl 22175 df-psr 22229 df-mvr 22230 df-mpl 22231 df-evls 22395

This theorem is used by: (None)

W3C validator