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 22128

Description: Lemma for evlseu 22130. 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 20272	. . . . . 6 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
3	1, 2	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Ring)
4	3	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring)
5		evlslem1.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
6		eqid 2740	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
7		evlslem1.c	. . . . . . . 8 ⊢ 𝐶 = (Base‘𝑆)
8	6, 7	rhmf 20511	. . . . . . 7 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶)
9	5, 8	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶𝐶)
10	9	adantr 480	. . . . 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 22041	. . . . . 6 ⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅))
16	15	ffvelcdmda 7118	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑌‘𝑏) ∈ (Base‘𝑅))
17	10, 16	ffvelcdmd 7119	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑌‘𝑏)) ∈ 𝐶)
18		evlslem1.t	. . . . . 6 ⊢ 𝑇 = (mulGrp‘𝑆)
19	18, 7	mgpbas 20167	. . . . 5 ⊢ 𝐶 = (Base‘𝑇)
20		evlslem1.x	. . . . 5 ⊢ ↑ = (._g‘𝑇)
21	18	crngmgp 20268	. . . . . . 7 ⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
22	1, 21	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ CMnd)
23	22	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd)
24		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷)
25		evlslem1.g	. . . . . 6 ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
26	25	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶)
27	13, 19, 20, 23, 24, 26	psrbagev2 22125	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)) ∈ 𝐶)
28		evlslem1.m	. . . . 5 ⊢ · = (._r‘𝑆)
29	7, 28	ringcl 20277	. . . 4 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘(𝑌‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)) ∈ 𝐶) → ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺))) ∈ 𝐶)
30	4, 17, 27, 29	syl3anc 1371	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺))) ∈ 𝐶)
31	30	fmpttd 7149	. 2 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))):𝐷⟶𝐶)
32		ovexd 7483	. . . . 5 ⊢ (𝜑 → (ℕ₀ ↑_m 𝐼) ∈ V)
33	13, 32	rabexd 5358	. . . 4 ⊢ (𝜑 → 𝐷 ∈ V)
34	33	mptexd 7261	. . 3 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) ∈ V)
35		funmpt 6616	. . . 4 ⊢ Fun (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺))))
36	35	a1i 11	. . 3 ⊢ (𝜑 → Fun (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))))
37		fvexd 6935	. . 3 ⊢ (𝜑 → (0_g‘𝑆) ∈ V)
38		eqid 2740	. . . . 5 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
39		evlslem1.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CRing)
40	11, 12, 38, 14, 39	mplelsfi 22038	. . . 4 ⊢ (𝜑 → 𝑌 finSupp (0_g‘𝑅))
41	40	fsuppimpd 9439	. . 3 ⊢ (𝜑 → (𝑌 supp (0_g‘𝑅)) ∈ Fin)
42	15	feqmptd 6990	. . . . . . 7 ⊢ (𝜑 → 𝑌 = (𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)))
43	42	oveq1d 7463	. . . . . 6 ⊢ (𝜑 → (𝑌 supp (0_g‘𝑅)) = ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0_g‘𝑅)))
44		eqimss2 4068	. . . . . 6 ⊢ ((𝑌 supp (0_g‘𝑅)) = ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0_g‘𝑅)) → ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0_g‘𝑅)) ⊆ (𝑌 supp (0_g‘𝑅)))
45	43, 44	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (𝑌‘𝑏)) supp (0_g‘𝑅)) ⊆ (𝑌 supp (0_g‘𝑅)))
46		rhmghm 20510	. . . . . 6 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
47		eqid 2740	. . . . . . 7 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
48	38, 47	ghmid 19262	. . . . . 6 ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘(0_g‘𝑅)) = (0_g‘𝑆))
49	5, 46, 48	3syl 18	. . . . 5 ⊢ (𝜑 → (𝐹‘(0_g‘𝑅)) = (0_g‘𝑆))
50		fvexd 6935	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑌‘𝑏) ∈ V)
51		fvexd 6935	. . . . 5 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
52	45, 49, 50, 51	suppssfv 8243	. . . 4 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (𝐹‘(𝑌‘𝑏))) supp (0_g‘𝑆)) ⊆ (𝑌 supp (0_g‘𝑅)))
53	7, 28, 47	ringlz 20316	. . . . 5 ⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ 𝐶) → ((0_g‘𝑆) · 𝑥) = (0_g‘𝑆))
54	3, 53	sylan 579	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((0_g‘𝑆) · 𝑥) = (0_g‘𝑆))
55		fvexd 6935	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑌‘𝑏)) ∈ V)
56	52, 54, 55, 27, 37	suppssov1 8238	. . 3 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) supp (0_g‘𝑆)) ⊆ (𝑌 supp (0_g‘𝑅)))
57		suppssfifsupp 9449	. . 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‘𝑆))
58	34, 36, 37, 41, 56, 57	syl32anc 1378	. 2 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) finSupp (0_g‘𝑆))
59	31, 58	jca 511	1 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σ_g (𝑏 ∘_f ↑ 𝐺)))) finSupp (0_g‘𝑆)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2108 {crab 3443 Vcvv 3488 ⊆ wss 3976 class class class wbr 5166 ↦ cmpt 5249 ^◡ccnv 5699 “ cima 5703 Fun wfun 6567 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 ∘_f cof 7712 supp csupp 8201 ↑_m cmap 8884 Fincfn 9003 finSupp cfsupp 9431 ℕcn 12293 ℕ₀cn0 12553 Basecbs 17258 ._rcmulr 17312 0_gc0g 17499 Σ_g cgsu 17500 ._gcmg 19107 GrpHom cghm 19252 CMndccmn 19822 mulGrpcmgp 20161 Ringcrg 20260 CRingccrg 20261 RingHom crh 20495 mVar cmvr 21948 mPoly cmpl 21949

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-om 7904 df-1st 8030 df-2nd 8031 df-supp 8202 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-er 8763 df-map 8886 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fsupp 9432 df-oi 9579 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-z 12640 df-uz 12904 df-fz 13568 df-fzo 13712 df-seq 14053 df-hash 14380 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-sca 17327 df-vsca 17328 df-tset 17330 df-0g 17501 df-gsum 17502 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-mhm 18818 df-grp 18976 df-minusg 18977 df-mulg 19108 df-ghm 19253 df-cntz 19357 df-cmn 19824 df-abl 19825 df-mgp 20162 df-rng 20180 df-ur 20209 df-ring 20262 df-cring 20263 df-rhm 20498 df-psr 21952 df-mpl 21954

This theorem is referenced by: evlslem1 22129

W3C validator