This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evlslem6

Description: Lemma for evlseu . 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)

Ref Expression
Hypotheses evlslem1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
evlslem1.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
evlslem1.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
evlslem1.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑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 evlslem6 ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 ∧ ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) finSupp ( 0g ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 evlslem1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 evlslem1.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 evlslem1.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
4 evlslem1.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
5 evlslem1.t ⊢ 𝑇 = ( mulGrp ‘ 𝑆 )
6 evlslem1.x ⊢ ↑ = ( .g ‘ 𝑇 )
7 evlslem1.m ⊢ · = ( .r ‘ 𝑆 )
8 evlslem1.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
9 evlslem1.e ⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
10 evlslem1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
11 evlslem1.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
12 evlslem1.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
13 evlslem1.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
14 evlslem1.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
15 evlslem6.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
16 crngring ⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
17 12 16 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ Ring )
19 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20 19 3 rhmf ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
21 13 20 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ 𝐶 )
23 1 19 2 4 15 mplelf ⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
24 23 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑌 ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
25 22 24 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) ∈ 𝐶 )
26 5 3 mgpbas ⊢ 𝐶 = ( Base ‘ 𝑇 )
27 5 crngmgp ⊢ ( 𝑆 ∈ CRing → 𝑇 ∈ CMnd )
28 12 27 syl ⊢ ( 𝜑 → 𝑇 ∈ CMnd )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑇 ∈ CMnd )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
31 14 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐺 : 𝐼 ⟶ 𝐶 )
32 4 26 6 29 30 31 psrbagev2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 )
33 3 7 ringcl ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) ∈ 𝐶 ∧ ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) → ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 )
34 18 25 32 33 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 )
35 34 fmpttd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 )
36 ovexd ⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
37 4 36 rabexd ⊢ ( 𝜑 → 𝐷 ∈ V )
38 37 mptexd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ∈ V )
39 funmpt ⊢ Fun ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
40 39 a1i ⊢ ( 𝜑 → Fun ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) )
41 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ V )
42 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
43 1 2 42 15 mplelsfi ⊢ ( 𝜑 → 𝑌 finSupp ( 0g ‘ 𝑅 ) )
44 43 fsuppimpd ⊢ ( 𝜑 → ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ∈ Fin )
45 23 feqmptd ⊢ ( 𝜑 → 𝑌 = ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) )
46 45 oveq1d ⊢ ( 𝜑 → ( 𝑌 supp ( 0g ‘ 𝑅 ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) supp ( 0g ‘ 𝑅 ) ) )
47 eqimss2 ⊢ ( ( 𝑌 supp ( 0g ‘ 𝑅 ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) supp ( 0g ‘ 𝑅 ) ) → ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) )
48 46 47 syl ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑌 ‘ 𝑏 ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) )
49 rhmghm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
50 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
51 42 50 ghmid ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
52 13 49 51 3syl ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
53 fvexd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑌 ‘ 𝑏 ) ∈ V )
54 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
55 48 52 53 54 suppssfv ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) )
56 3 7 50 ringlz ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑥 ∈ 𝐶 ) → ( ( 0g ‘ 𝑆 ) · 𝑥 ) = ( 0g ‘ 𝑆 ) )
57 17 56 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 0g ‘ 𝑆 ) · 𝑥 ) = ( 0g ‘ 𝑆 ) )
58 fvexd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) ∈ V )
59 55 57 58 32 41 suppssov1 ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) )
60 suppssfifsupp ⊢ ( ( ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ∈ V ∧ Fun ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ∧ ( 0g ‘ 𝑆 ) ∈ V ) ∧ ( ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ∈ Fin ∧ ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )
61 38 40 41 44 59 60 syl32anc ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )
62 35 61 jca ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 ∧ ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑌 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) finSupp ( 0g ‘ 𝑆 ) ) )