Theorem evl1gsumadd

Description: Univariate polynomial evaluation maps (additive) group sums to group sums. Remark: the proof would be shorter if the theorem is proved directly instead of using evls1gsumadd . (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 )
	evl1gsumadd.0	⊢ 0 = ( 0g ‘ 𝑊 )
	evl1gsumadd.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) finSupp 0 )
Assertion	evl1gsumadd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σ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		evl1gsumadd.0	⊢ 0 = ( 0g ‘ 𝑊 )
10		evl1gsumadd.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) finSupp 0 )
11	1 2	evl1fval1	⊢ 𝑄 = ( 𝑅 evalSub1 𝐾 )
12	11	a1i	⊢ ( 𝜑 → 𝑄 = ( 𝑅 evalSub1 𝐾 ) )
13	12	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) = ( ( 𝑅 evalSub1 𝐾 ) ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) )
14	2	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐾 ) = 𝑅 )
15	6 14	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐾 ) = 𝑅 )
16	15	eqcomd	⊢ ( 𝜑 → 𝑅 = ( 𝑅 ↾s 𝐾 ) )
17	16	fveq2d	⊢ ( 𝜑 → ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) )
18	3 17	syl5eq	⊢ ( 𝜑 → 𝑊 = ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) )
19	18	fvoveq1d	⊢ ( 𝜑 → ( ( 𝑅 evalSub1 𝐾 ) ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) = ( ( 𝑅 evalSub1 𝐾 ) ‘ ( ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) )
20		eqid	⊢ ( 𝑅 evalSub1 𝐾 ) = ( 𝑅 evalSub1 𝐾 )
21		eqid	⊢ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) = ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) )
22		eqid	⊢ ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) ) = ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) )
23		eqid	⊢ ( 𝑅 ↾s 𝐾 ) = ( 𝑅 ↾s 𝐾 )
24		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) )
25		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
26	2	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐾 ∈ ( SubRing ‘ 𝑅 ) )
27	6 25 26	3syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubRing ‘ 𝑅 ) )
28	18	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝑊 = ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) )
29	28	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( Base ‘ 𝑊 ) = ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) ) )
30	5 29	syl5eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝐵 = ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) ) )
31	7 30	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) ) )
32	18	eqcomd	⊢ ( 𝜑 → ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) = 𝑊 )
33	32	fveq2d	⊢ ( 𝜑 → ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) ) = ( 0g ‘ 𝑊 ) )
34	33 9	eqtr4di	⊢ ( 𝜑 → ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) ) = 0 )
35	10 34	breqtrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) finSupp ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) ) )
36	20 2 21 22 23 4 24 6 27 31 8 35	evls1gsumadd	⊢ ( 𝜑 → ( ( 𝑅 evalSub1 𝐾 ) ‘ ( ( Poly1 ‘ ( 𝑅 ↾s 𝐾 ) ) Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) ) ) )
37	19 36	eqtrd	⊢ ( 𝜑 → ( ( 𝑅 evalSub1 𝐾 ) ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) ) ) )
38	12	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑌 ) = ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) )
39	38	eqcomd	⊢ ( 𝜑 → ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) = ( 𝑄 ‘ 𝑌 ) )
40	39	mpteq2dv	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ 𝑁 ↦ ( 𝑄 ‘ 𝑌 ) ) )
41	40	oveq2d	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥 ∈ 𝑁 ↦ ( 𝑄 ‘ 𝑌 ) ) ) )
42	13 37 41	3eqtrd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥 ∈ 𝑁 ↦ ( 𝑄 ‘ 𝑌 ) ) ) )