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 ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) )