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

Metamath Proof Explorer

Theorem evls1gsummul

Description: Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 14-Sep-2019)

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

Proof

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