Theorem gsumply1subr

Description: Evaluate a group sum in a polynomial ring over a subring. (Contributed by AV, 22-Sep-2019) (Proof shortened by AV, 31-Jan-2020)

	Ref	Expression
Hypotheses	subrgply1.s	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
	subrgply1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	subrgply1.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
	subrgply1.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
	gsumply1subr.s	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	gsumply1subr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumply1subr.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	gsumply1subr	⊢ ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( 𝑈 Σg 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		subrgply1.s	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
2		subrgply1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3		subrgply1.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
4		subrgply1.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		gsumply1subr.s	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6		gsumply1subr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7		gsumply1subr.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8	1 2 3 4	subrgply1	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
9		subrgsubg	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubGrp ‘ 𝑆 ) )
10		subgsubm	⊢ ( 𝐵 ∈ ( SubGrp ‘ 𝑆 ) → 𝐵 ∈ ( SubMnd ‘ 𝑆 ) )
11	9 10	syl	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubMnd ‘ 𝑆 ) )
12	5 8 11	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubMnd ‘ 𝑆 ) )
13		eqid	⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
14	6 12 7 13	gsumsubm	⊢ ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( ( 𝑆 ↾s 𝐵 ) Σg 𝐹 ) )
15	7 6	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
16		ovexd	⊢ ( 𝜑 → ( 𝑆 ↾s 𝐵 ) ∈ V )
17	3	fvexi	⊢ 𝑈 ∈ V
18	17	a1i	⊢ ( 𝜑 → 𝑈 ∈ V )
19		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
20	4	oveq2i	⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s ( Base ‘ 𝑈 ) )
21	1 2 3 19 5 20	ressply1bas	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) )
22	21	eqcomd	⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) = ( Base ‘ 𝑈 ) )
23	13	subrgring	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑆 ↾s 𝐵 ) ∈ Ring )
24	8 23	syl	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑆 ↾s 𝐵 ) ∈ Ring )
25		ringmgm	⊢ ( ( 𝑆 ↾s 𝐵 ) ∈ Ring → ( 𝑆 ↾s 𝐵 ) ∈ Mgm )
26	5 24 25	3syl	⊢ ( 𝜑 → ( 𝑆 ↾s 𝐵 ) ∈ Mgm )
27		simpl	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → 𝜑 )
28	1 2 3 4 5 13	ressply1bas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) )
29	28	eqcomd	⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) = 𝐵 )
30	29	eleq2d	⊢ ( 𝜑 → ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ↔ 𝑠 ∈ 𝐵 ) )
31	30	biimpcd	⊢ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) → ( 𝜑 → 𝑠 ∈ 𝐵 ) )
32	31	adantr	⊢ ( ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) → ( 𝜑 → 𝑠 ∈ 𝐵 ) )
33	32	impcom	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → 𝑠 ∈ 𝐵 )
34	29	eleq2d	⊢ ( 𝜑 → ( 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ↔ 𝑡 ∈ 𝐵 ) )
35	34	biimpcd	⊢ ( 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) → ( 𝜑 → 𝑡 ∈ 𝐵 ) )
36	35	adantl	⊢ ( ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) → ( 𝜑 → 𝑡 ∈ 𝐵 ) )
37	36	impcom	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → 𝑡 ∈ 𝐵 )
38	1 2 3 4 5 13	ressply1add	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ) → ( 𝑠 ( +g ‘ 𝑈 ) 𝑡 ) = ( 𝑠 ( +g ‘ ( 𝑆 ↾s 𝐵 ) ) 𝑡 ) )
39	27 33 37 38	syl12anc	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → ( 𝑠 ( +g ‘ 𝑈 ) 𝑡 ) = ( 𝑠 ( +g ‘ ( 𝑆 ↾s 𝐵 ) ) 𝑡 ) )
40	39	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → ( 𝑠 ( +g ‘ ( 𝑆 ↾s 𝐵 ) ) 𝑡 ) = ( 𝑠 ( +g ‘ 𝑈 ) 𝑡 ) )
41	7	ffund	⊢ ( 𝜑 → Fun 𝐹 )
42	7	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
43	42 28	sseqtrd	⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) )
44	15 16 18 22 26 40 41 43	gsummgmpropd	⊢ ( 𝜑 → ( ( 𝑆 ↾s 𝐵 ) Σg 𝐹 ) = ( 𝑈 Σg 𝐹 ) )
45	14 44	eqtrd	⊢ ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( 𝑈 Σg 𝐹 ) )