evlslem6 - Metamath Proof Explorer

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

Theorem evlslem6 22203

Description: Lemma for evlseu 22205. Finiteness and consistency of the top-level sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.)

**Hypotheses**
Ref	Expression
evlslem1.p	⊢ 𝑃 = (𝐼 mPoly 𝑅)
evlslem1.b	⊢ 𝐵 = (Base‘𝑃)
evlslem1.c	⊢ 𝐶 = (Base‘𝑆)
evlslem1.d	⊢ 𝐷 = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
evlslem1.t	⊢ 𝑇 = (mulGrp‘𝑆)
evlslem1.x	⊢ ↑ = (._g‘𝑇)
evlslem1.m	⊢ · = (._r‘𝑆)
evlslem1.v	⊢ 𝑉 = (𝐼 mVar 𝑅)
evlslem1.e	⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺))))))
evlslem1.i	⊢ (𝜑 → 𝐼 ∈ 𝑊)
evlslem1.r	⊢ (𝜑 → 𝑅 ∈ CRing)
evlslem1.s	⊢ (𝜑 → 𝑆 ∈ CRing)
evlslem1.f	⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
evlslem1.g	⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
evlslem6.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)

**Assertion**
Ref	Expression
evlslem6	⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) finSupp (0_g‘𝑆)))

Distinct variable groups: 𝜑,𝑏 𝐶,𝑏 𝐷,𝑏 ℎ,𝐼 𝑅,𝑏 𝑆,𝑏 𝑌,𝑏 ℎ,𝑏 Allowed substitution hints: 𝜑(ℎ,𝑝) 𝐵(ℎ,𝑝,𝑏) 𝐶(ℎ,𝑝) 𝐷(ℎ,𝑝) 𝑃(ℎ,𝑝,𝑏) 𝑅(ℎ,𝑝) 𝑆(ℎ,𝑝) 𝑇(ℎ,𝑝,𝑏) · (ℎ,𝑝,𝑏) 𝐸(ℎ,𝑝,𝑏) ↑ (ℎ,𝑝,𝑏) 𝐹(ℎ,𝑝,𝑏) 𝐺(ℎ,𝑝,𝑏) 𝐼(𝑝,𝑏) 𝑉(ℎ,𝑝,𝑏) 𝑊(ℎ,𝑝,𝑏) 𝑌(ℎ,𝑝)

Proof of Theorem evlslem6 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlslem1.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ CRing)
2		crngring 20329	. . . . . 6 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
3	1, 2	syl 18	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Ring)
4	3	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring)
5		evlslem1.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
6		eqid 2769	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
7		evlslem1.c	. . . . . . . 8 ⊢ 𝐶 = (Base‘𝑆)
8	6, 7	rhmf 20568	. . . . . . 7 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶)
9	5, 8	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶𝐶)
10	9	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐹:(Base‘𝑅)⟶𝐶)
11		evlslem1.p	. . . . . . 7 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
12		evlslem1.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑃)
13		evlslem1.d	. . . . . . 7 ⊢ 𝐷 = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
14		evlslem6.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
15	11, 6, 12, 13, 14	mplelf 22118	. . . . . 6 ⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅))
16	15	ffvelcdmda 7082	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑌‘𝑏) ∈ (Base‘𝑅))
17	10, 16	ffvelcdmd 7083	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑌‘𝑏)) ∈ 𝐶)
18		evlslem1.t	. . . . . 6 ⊢ 𝑇 = (mulGrp‘𝑆)
19	18, 7	mgpbas 20223	. . . . 5 ⊢ 𝐶 = (Base‘𝑇)
20		evlslem1.x	. . . . 5 ⊢ ↑ = (._g‘𝑇)
21	18	crngmgp 20325	. . . . . . 7 ⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
22	1, 21	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ CMnd)
23	22	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd)
24		simpr 489	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷)
25		evlslem1.g	. . . . . 6 ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
26	25	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶)
27	13, 19, 20, 23, 24, 26	psrbagev2 22200	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)) ∈ 𝐶)
28		evlslem1.m	. . . . 5 ⊢ · = (._r‘𝑆)
29	7, 28	ringcl 20334	. . . 4 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘(𝑌‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)) ∈ 𝐶) → ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺))) ∈ 𝐶)
30	4, 17, 27, 29	syl3anc 1396	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺))) ∈ 𝐶)
31	30	fmpttd 7113	. 2 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))):𝐷⟶𝐶)
32		ovexd 7448	. . . . 5 ⊢ (𝜑 → (ℕ₀ ↑_m 𝐼) ∈ V)
33	13, 32	rabexd 5313	. . . 4 ⊢ (𝜑 → 𝐷 ∈ V)
34	33	mptexd 7225	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) ∈ V)
35		funmpt 6577	. . . 4 ⊢ Fun (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺))))
36	35	a1i 11	. . 3 ⊢ (𝜑 → Fun (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))))
37		fvexd 6899	. . 3 ⊢ (𝜑 → (0_g‘𝑆) ∈ V)
38		eqid 2769	. . . . 5 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
39	11, 12, 38, 14	mplelsfi 22115	. . . 4 ⊢ (𝜑 → 𝑌 finSupp (0_g‘𝑅))
40	39	fsuppimpd 9331	. . 3 ⊢ (𝜑 → (𝑌 supp (0_g‘𝑅)) ∈ Fin)
41	15	feqmptd 6952	. . . . . . 7 ⊢ (𝜑 → 𝑌 = (𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)))
42	41	oveq1d 7428	. . . . . 6 ⊢ (𝜑 → (𝑌 supp (0_g‘𝑅)) = ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0_g‘𝑅)))
43		eqimss2 4004	. . . . . 6 ⊢ ((𝑌 supp (0_g‘𝑅)) = ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0_g‘𝑅)) → ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0_g‘𝑅)) ⊆ (𝑌 supp (0_g‘𝑅)))
44	42, 43	syl 18	. . . . 5 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0_g‘𝑅)) ⊆ (𝑌 supp (0_g‘𝑅)))
45		rhmghm 20567	. . . . . 6 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
46		eqid 2769	. . . . . . 7 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
47	38, 46	ghmid 19294	. . . . . 6 ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘(0_g‘𝑅)) = (0_g‘𝑆))
48	5, 45, 47	3syl 19	. . . . 5 ⊢ (𝜑 → (𝐹‘(0_g‘𝑅)) = (0_g‘𝑆))
49		fvexd 6899	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑌‘𝑏) ∈ V)
50		fvexd 6899	. . . . 5 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
51	44, 48, 49, 50	suppssfv 8200	. . . 4 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (𝐹‘(𝑌‘𝑏))) supp (0_g‘𝑆)) ⊆ (𝑌 supp (0_g‘𝑅)))
52	7, 28, 46	ringlz 20378	. . . . 5 ⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ 𝐶) → ((0_g‘𝑆) · 𝑥) = (0_g‘𝑆))
53	3, 52	sylan 591	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((0_g‘𝑆) · 𝑥) = (0_g‘𝑆))
54		fvexd 6899	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑌‘𝑏)) ∈ V)
55	51, 53, 54, 27, 37	suppssov1 8195	. . 3 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) supp (0_g‘𝑆)) ⊆ (𝑌 supp (0_g‘𝑅)))
56		suppssfifsupp 9342	. . 3 ⊢ ((((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) ∈ V ∧ Fun (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) ∧ (0_g‘𝑆) ∈ V) ∧ ((𝑌 supp (0_g‘𝑅)) ∈ Fin ∧ ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) supp (0_g‘𝑆)) ⊆ (𝑌 supp (0_g‘𝑅)))) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) finSupp (0_g‘𝑆))
57	34, 36, 37, 40, 55, 56	syl32anc 1403	. 2 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) finSupp (0_g‘𝑆))
58	31, 57	jca 520	1 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) finSupp (0_g‘𝑆)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 ∈ wcel 2149 {crab 3423 Vcvv 3463 ⊆ wss 3913 class class class wbr 5113 ↦ cmpt 5196 ^◡ccnv 5663 “ cima 5667 Fun wfun 6533 ⟶wf 6535 ‘cfv 6539 (class class class)co 7413 ∘_f cof 7675 supp csupp 8158 ↑_m cmap 8826 Fincfn 8945 finSupp cfsupp 9323 ℕcn 12235 ℕ₀cn0 12506 Basecbs 17271 ._rcmulr 17313 0_gc0g 17494 Σ_g cgsu 17495 ._gcmg 19135 GrpHom cghm 19285 CMndccmn 19852 mulGrpcmgp 20218 Ringcrg 20317 CRingccrg 20318 RingHom crh 20553 mVar cmvr 22026 mPoly cmpl 22027

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5273 ax-pow 5339 ax-pr 5407 ax-un 7735 ax-cnex 11158 ax-resscn 11159 ax-1cn 11160 ax-icn 11161 ax-addcl 11162 ax-addrcl 11163 ax-mulcl 11164 ax-mulrcl 11165 ax-mulcom 11166 ax-addass 11167 ax-mulass 11168 ax-distr 11169 ax-i2m1 11170 ax-1ne0 11171 ax-1rid 11172 ax-rnegex 11173 ax-rrecex 11174 ax-cnre 11175 ax-pre-lttri 11176 ax-pre-lttrn 11177 ax-pre-ltadd 11178 ax-pre-mulgt0 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5559 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 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 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7677 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-er 8696 df-map 8828 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9324 df-oi 9474 df-card 9927 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11445 df-neg 11446 df-nn 12236 df-2 12305 df-3 12306 df-4 12307 df-5 12308 df-6 12309 df-7 12310 df-8 12311 df-9 12312 df-n0 12507 df-z 12594 df-uz 12865 df-fz 13538 df-fzo 13685 df-seq 14040 df-hash 14369 df-struct 17209 df-sets 17226 df-slot 17244 df-ndx 17256 df-base 17272 df-ress 17293 df-plusg 17325 df-mulr 17326 df-sca 17328 df-vsca 17329 df-tset 17331 df-0g 17496 df-gsum 17497 df-mgm 18700 df-sgrp 18779 df-mnd 18795 df-mhm 18843 df-grp 19005 df-minusg 19006 df-mulg 19136 df-ghm 19286 df-cntz 19389 df-cmn 19854 df-abl 19855 df-mgp 20219 df-rng 20233 df-ur 20266 df-ring 20319 df-cring 20320 df-rhm 20556 df-psr 22030 df-mpl 22032

This theorem is referenced by: evlslem1 22204

W3C validator