Theorem evl1gsummon

Description: Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019)

	Ref	Expression
Hypotheses	evl1gsummon.q	⊢ 𝑄 = ( eval1 ‘ 𝑅 )
	evl1gsummon.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	evl1gsummon.w	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
	evl1gsummon.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	evl1gsummon.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	evl1gsummon.h	⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
	evl1gsummon.e	⊢ 𝐸 = ( .g ‘ 𝐻 )
	evl1gsummon.g	⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
	evl1gsummon.p	⊢ ↑ = ( .g ‘ 𝐺 )
	evl1gsummon.t1	⊢ × = ( ·𝑠 ‘ 𝑊 )
	evl1gsummon.t2	⊢ · = ( .r ‘ 𝑅 )
	evl1gsummon.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evl1gsummon.a	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 𝐴 ∈ 𝐾 )
	evl1gsummon.m	⊢ ( 𝜑 → 𝑀 ⊆ ℕ0 )
	evl1gsummon.f	⊢ ( 𝜑 → 𝑀 ∈ Fin )
	evl1gsummon.n	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 𝑁 ∈ ℕ0 )
	evl1gsummon.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion	evl1gsummon	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ) ) ‘ 𝐶 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evl1gsummon.q	⊢ 𝑄 = ( eval1 ‘ 𝑅 )
2		evl1gsummon.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		evl1gsummon.w	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
4		evl1gsummon.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
5		evl1gsummon.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
6		evl1gsummon.h	⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
7		evl1gsummon.e	⊢ 𝐸 = ( .g ‘ 𝐻 )
8		evl1gsummon.g	⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
9		evl1gsummon.p	⊢ ↑ = ( .g ‘ 𝐺 )
10		evl1gsummon.t1	⊢ × = ( ·𝑠 ‘ 𝑊 )
11		evl1gsummon.t2	⊢ · = ( .r ‘ 𝑅 )
12		evl1gsummon.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
13		evl1gsummon.a	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 𝐴 ∈ 𝐾 )
14		evl1gsummon.m	⊢ ( 𝜑 → 𝑀 ⊆ ℕ0 )
15		evl1gsummon.f	⊢ ( 𝜑 → 𝑀 ∈ Fin )
16		evl1gsummon.n	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 𝑁 ∈ ℕ0 )
17		evl1gsummon.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
18		eqid	⊢ ( 𝑅 ↑s 𝐾 ) = ( 𝑅 ↑s 𝐾 )
19		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
20	12 19	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
21	3	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ LMod )
22	20 21	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑊 ∈ LMod )
24	13	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐴 ∈ 𝐾 )
25	3	ply1sca	⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑊 ) )
26	12 25	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
27	26	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
28	2 27	eqtrid	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
30	24 29	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
31	8 4	mgpbas	⊢ 𝐵 = ( Base ‘ 𝐺 )
32	3	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
33	20 32	syl	⊢ ( 𝜑 → 𝑊 ∈ Ring )
34	8	ringmgp	⊢ ( 𝑊 ∈ Ring → 𝐺 ∈ Mnd )
35	33 34	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐺 ∈ Mnd )
37	16	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑁 ∈ ℕ0 )
38	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑅 ∈ Ring )
39	5 3 4	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
40	38 39	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑋 ∈ 𝐵 )
41	31 9 36 37 40	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝑁 ↑ 𝑋 ) ∈ 𝐵 )
42		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
43		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
44	4 42 10 43	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑁 ↑ 𝑋 ) ∈ 𝐵 ) → ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ∈ 𝐵 )
45	23 30 41 44	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ∈ 𝐵 )
46	1 2 3 18 4 12 45 14 15 17	evl1gsumaddval	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ) ) ‘ 𝐶 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) ) ) )
47	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑅 ∈ CRing )
48	17	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐶 ∈ 𝐾 )
49	1 3 8 5 2 9 47 37 10 24 48 6 7 11	evl1scvarpwval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) = ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) )
50	49	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑀 ↦ ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) ) = ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) )
51	50	oveq2d	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) ) )
52	46 51	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ) ) ‘ 𝐶 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝑀 ↦ ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) ) )