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