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		fex	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
16	7 6 15	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
17		ovexd	⊢ ( 𝜑 → ( 𝑆 ↾s 𝐵 ) ∈ V )
18	3	fvexi	⊢ 𝑈 ∈ V
19	18	a1i	⊢ ( 𝜑 → 𝑈 ∈ V )
20		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
21	4	oveq2i	⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s ( Base ‘ 𝑈 ) )
22	1 2 3 20 5 21	ressply1bas	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) )
23	22	eqcomd	⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) = ( Base ‘ 𝑈 ) )
24	13	subrgring	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑆 ↾s 𝐵 ) ∈ Ring )
25	8 24	syl	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑆 ↾s 𝐵 ) ∈ Ring )
26		ringmgm	⊢ ( ( 𝑆 ↾s 𝐵 ) ∈ Ring → ( 𝑆 ↾s 𝐵 ) ∈ Mgm )
27	5 25 26	3syl	⊢ ( 𝜑 → ( 𝑆 ↾s 𝐵 ) ∈ Mgm )
28		simpl	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → 𝜑 )
29	1 2 3 4 5 13	ressply1bas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) )
30	29	eqcomd	⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) = 𝐵 )
31	30	eleq2d	⊢ ( 𝜑 → ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ↔ 𝑠 ∈ 𝐵 ) )
32	31	biimpcd	⊢ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) → ( 𝜑 → 𝑠 ∈ 𝐵 ) )
33	32	adantr	⊢ ( ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) → ( 𝜑 → 𝑠 ∈ 𝐵 ) )
34	33	impcom	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → 𝑠 ∈ 𝐵 )
35	30	eleq2d	⊢ ( 𝜑 → ( 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ↔ 𝑡 ∈ 𝐵 ) )
36	35	biimpcd	⊢ ( 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) → ( 𝜑 → 𝑡 ∈ 𝐵 ) )
37	36	adantl	⊢ ( ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) → ( 𝜑 → 𝑡 ∈ 𝐵 ) )
38	37	impcom	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → 𝑡 ∈ 𝐵 )
39	1 2 3 4 5 13	ressply1add	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ) → ( 𝑠 ( +g ‘ 𝑈 ) 𝑡 ) = ( 𝑠 ( +g ‘ ( 𝑆 ↾s 𝐵 ) ) 𝑡 ) )
40	28 34 38 39	syl12anc	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → ( 𝑠 ( +g ‘ 𝑈 ) 𝑡 ) = ( 𝑠 ( +g ‘ ( 𝑆 ↾s 𝐵 ) ) 𝑡 ) )
41	40	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) ) ) → ( 𝑠 ( +g ‘ ( 𝑆 ↾s 𝐵 ) ) 𝑡 ) = ( 𝑠 ( +g ‘ 𝑈 ) 𝑡 ) )
42	7	ffund	⊢ ( 𝜑 → Fun 𝐹 )
43	7	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
44	43 29	sseqtrd	⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ ( 𝑆 ↾s 𝐵 ) ) )
45	16 17 19 23 27 41 42 44	gsummgmpropd	⊢ ( 𝜑 → ( ( 𝑆 ↾s 𝐵 ) Σg 𝐹 ) = ( 𝑈 Σg 𝐹 ) )
46	14 45	eqtrd	⊢ ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( 𝑈 Σg 𝐹 ) )