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

Metamath Proof Explorer

Theorem evlsgsummul

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

Ref Expression
Hypotheses evlsgsummul.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsgsummul.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
evlsgsummul.g ⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
evlsgsummul.1 ⊢ 1 = ( 1r ‘ 𝑊 )
evlsgsummul.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsgsummul.p ⊢ 𝑃 = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
evlsgsummul.h ⊢ 𝐻 = ( mulGrp ‘ 𝑃 )
evlsgsummul.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
evlsgsummul.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
evlsgsummul.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlsgsummul.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsgsummul.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlsgsummul.y ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝑌 ∈ 𝐵 )
evlsgsummul.n ⊢ ( 𝜑 → 𝑁 ⊆ ℕ0 )
evlsgsummul.f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) finSupp 1 )
Assertion evlsgsummul ( 𝜑 → ( 𝑄 ‘ ( 𝐺 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ 𝑁 ↦ ( 𝑄 ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 evlsgsummul.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsgsummul.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
3 evlsgsummul.g ⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
4 evlsgsummul.1 ⊢ 1 = ( 1r ‘ 𝑊 )
5 evlsgsummul.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
6 evlsgsummul.p ⊢ 𝑃 = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
7 evlsgsummul.h ⊢ 𝐻 = ( mulGrp ‘ 𝑃 )
8 evlsgsummul.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
9 evlsgsummul.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
10 evlsgsummul.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11 evlsgsummul.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
12 evlsgsummul.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
13 evlsgsummul.y ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝑌 ∈ 𝐵 )
14 evlsgsummul.n ⊢ ( 𝜑 → 𝑁 ⊆ ℕ0 )
15 evlsgsummul.f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) finSupp 1 )
16 3 9 mgpbas ⊢ 𝐵 = ( Base ‘ 𝐺 )
17 3 4 ringidval ⊢ 1 = ( 0g ‘ 𝐺 )
18 5 subrgcrng ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
19 11 12 18 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
20 2 mplcrng ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑈 ∈ CRing ) → 𝑊 ∈ CRing )
21 10 19 20 syl2anc ⊢ ( 𝜑 → 𝑊 ∈ CRing )
22 3 crngmgp ⊢ ( 𝑊 ∈ CRing → 𝐺 ∈ CMnd )
23 21 22 syl ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
24 crngring ⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
25 11 24 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
26 ovex ⊢ ( 𝐾 ↑m 𝐼 ) ∈ V
27 25 26 jctir ⊢ ( 𝜑 → ( 𝑆 ∈ Ring ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) )
28 6 pwsring ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → 𝑃 ∈ Ring )
29 7 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝐻 ∈ Mnd )
30 27 28 29 3syl ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
31 nn0ex ⊢ ℕ0 ∈ V
32 31 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
33 32 14 ssexd ⊢ ( 𝜑 → 𝑁 ∈ V )
34 1 2 5 6 8 evlsrhm ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) )
35 10 11 12 34 syl3anc ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) )
36 3 7 rhmmhm ⊢ ( 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) → 𝑄 ∈ ( 𝐺 MndHom 𝐻 ) )
37 35 36 syl ⊢ ( 𝜑 → 𝑄 ∈ ( 𝐺 MndHom 𝐻 ) )
38 16 17 23 30 33 37 13 15 gsummptmhm ⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑥 ∈ 𝑁 ↦ ( 𝑄 ‘ 𝑌 ) ) ) = ( 𝑄 ‘ ( 𝐺 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) )
39 38 eqcomd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐺 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ 𝑁 ↦ ( 𝑄 ‘ 𝑌 ) ) ) )