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 22406

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 20827	. . . . . 6 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
8	5, 7	syl 18	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ Ring)
9	3, 4, 8	mplringd 22331	. . . 4 ⊢ (𝜑 → 𝑊 ∈ Ring)
10		ringcmn 20512	. . . 4 ⊢ (𝑊 ∈ Ring → 𝑊 ∈ CMnd)
11	9, 10	syl 18	. . 3 ⊢ (𝜑 → 𝑊 ∈ CMnd)
12		evlsgsumadd.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ CRing)
13		crngring 20473	. . . . . 6 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
14	12, 13	syl 18	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Ring)
15		ovex 7454	. . . . 5 ⊢ (𝐾 ↑_m 𝐼) ∈ V
16	14, 15	jctir 530	. . . 4 ⊢ (𝜑 → (𝑆 ∈ Ring ∧ (𝐾 ↑_m 𝐼) ∈ V))
17		evlsgsumadd.p	. . . . 5 ⊢ 𝑃 = (𝑆 ↑_s (𝐾 ↑_m 𝐼))
18	17	pwsring 20554	. . . 4 ⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑_m 𝐼) ∈ V) → 𝑃 ∈ Ring)
19		ringmnd 20471	. . . 4 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
20	16, 18, 19	3syl 19	. . 3 ⊢ (𝜑 → 𝑃 ∈ Mnd)
21		nn0ex 12613	. . . . 5 ⊢ ℕ₀ ∈ V
22	21	a1i 11	. . . 4 ⊢ (𝜑 → ℕ₀ ∈ V)
23		evlsgsumadd.n	. . . 4 ⊢ (𝜑 → 𝑁 ⊆ ℕ₀)
24	22, 23	ssexd 5286	. . 3 ⊢ (𝜑 → 𝑁 ∈ V)
25		evlsgsumadd.q	. . . . . 6 ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
26		evlsgsumadd.k	. . . . . 6 ⊢ 𝐾 = (Base‘𝑆)
27	25, 3, 6, 17, 26	evlsrhm 22398	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom 𝑃))
28	4, 12, 5, 27	syl3anc 1398	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom 𝑃))
29		rhmghm 20715	. . . 4 ⊢ (𝑄 ∈ (𝑊 RingHom 𝑃) → 𝑄 ∈ (𝑊 GrpHom 𝑃))
30		ghmmhm 19441	. . . 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 20155	. 2 ⊢ (𝜑 → (𝑃 Σ_g (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))) = (𝑄‘(𝑊 Σ_g (𝑥 ∈ 𝑁 ↦ 𝑌))))
35	34	eqcomd 2767	1 ⊢ (𝜑 → (𝑄‘(𝑊 Σ_g (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σ_g (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 Vcvv 3451 ⊆ wss 3914 class class class wbr 5103 ↦ cmpt 5186 ‘cfv 6539 (class class class)co 7421 ↑_m cmap 8848 finSupp cfsupp 9354 ℕ₀cn0 12607 Basecbs 17388 ↾_s cress 17409 0_gc0g 17611 Σ_g cgsu 17612 ↑_s cpws 17618 Mndcmnd 18924 MndHom cmhm 18977 GrpHom cghm 19428 CMndccmn 19995 Ringcrg 20460 CRingccrg 20461 RingHom crh 20700 SubRingcsubrg 20822 mPoly cmpl 22215 evalSub ces 22382

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7752 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3900 df-un 3902 df-in 3904 df-ss 3915 df-pss 4035 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6305 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6495 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-of 7694 df-ofr 7695 df-om 7879 df-1st 8002 df-2nd 8003 df-supp 8179 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-2o 8478 df-er 8718 df-map 8850 df-pm 8851 df-ixp 8927 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-fsupp 9355 df-sup 9435 df-oi 9505 df-card 10021 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-nn 12337 df-2 12406 df-3 12407 df-4 12408 df-5 12409 df-6 12410 df-7 12411 df-8 12412 df-9 12413 df-n0 12608 df-z 12695 df-dec 12816 df-uz 12967 df-fz 13641 df-fzo 13790 df-seq 14146 df-hash 14476 df-struct 17326 df-sets 17343 df-slot 17361 df-ndx 17373 df-base 17389 df-ress 17410 df-plusg 17442 df-mulr 17443 df-sca 17445 df-vsca 17446 df-ip 17447 df-tset 17448 df-ple 17449 df-ds 17451 df-hom 17453 df-cco 17454 df-0g 17613 df-gsum 17614 df-prds 17619 df-pws 17621 df-mre 17757 df-mrc 17758 df-acs 17760 df-mgm 18817 df-sgrp 18909 df-mnd 18925 df-mhm 18979 df-submnd 18980 df-grp 19148 df-minusg 19149 df-sbg 19150 df-mulg 19279 df-subg 19334 df-ghm 19429 df-cntz 19532 df-cmn 19997 df-abl 19998 df-mgp 20362 df-rng 20376 df-ur 20409 df-srg 20414 df-ring 20462 df-cring 20463 df-rhm 20703 df-subrng 20799 df-subrg 20823 df-lmod 21138 df-lss 21208 df-lsp 21248 df-assa 22162 df-asp 22163 df-ascl 22164 df-psr 22218 df-mvr 22219 df-mpl 22220 df-evls 22384

This theorem is used by: (None)

W3C validator