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

Metamath Proof Explorer

Theorem evl1gsummul

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

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

Proof

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