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	$⊢ S = {Poly}_{1} (R)$
	subrgply1.h	$⊢ H = R ↾_{𝑠} T$
	subrgply1.u	$⊢ U = {Poly}_{1} (H)$
	subrgply1.b	$⊢ B = {Base}_{U}$
	gsumply1subr.s	$⊢ φ \to T \in SubRing (R)$
	gsumply1subr.a	$⊢ φ \to A \in V$
	gsumply1subr.f	$⊢ φ \to F : A ⟶ B$
Assertion	gsumply1subr	$⊢ φ \to \sum_{S} F = \sum_{U} F$

Proof

Step	Hyp	Ref	Expression
1		subrgply1.s	$⊢ S = {Poly}_{1} (R)$
2		subrgply1.h	$⊢ H = R ↾_{𝑠} T$
3		subrgply1.u	$⊢ U = {Poly}_{1} (H)$
4		subrgply1.b	$⊢ B = {Base}_{U}$
5		gsumply1subr.s	$⊢ φ \to T \in SubRing (R)$
6		gsumply1subr.a	$⊢ φ \to A \in V$
7		gsumply1subr.f	$⊢ φ \to F : A ⟶ B$
8	1 2 3 4	subrgply1	$⊢ T \in SubRing (R) \to B \in SubRing (S)$
9		subrgsubg	$⊢ B \in SubRing (S) \to B \in SubGrp (S)$
10		subgsubm	$⊢ B \in SubGrp (S) \to B \in SubMnd (S)$
11	5 8 9 10	4syl	$⊢ φ \to B \in SubMnd (S)$
12		eqid	$⊢ S ↾_{𝑠} B = S ↾_{𝑠} B$
13	6 11 7 12	gsumsubm	$⊢ φ \to \sum_{S} F = \sum_{S ↾_{𝑠} B} F$
14	7 6	fexd	$⊢ φ \to F \in V$
15		ovexd	$⊢ φ \to S ↾_{𝑠} B \in V$
16	3	fvexi	$⊢ U \in V$
17	16	a1i	$⊢ φ \to U \in V$
18		eqid	$⊢ {Base}_{U} = {Base}_{U}$
19	4	oveq2i	$⊢ S ↾_{𝑠} B = S ↾_{𝑠} {Base}_{U}$
20	1 2 3 18 5 19	ressply1bas	$⊢ φ \to {Base}_{U} = {Base}_{(S ↾_{𝑠} B)}$
21	20	eqcomd	$⊢ φ \to {Base}_{(S ↾_{𝑠} B)} = {Base}_{U}$
22	12	subrgring	$⊢ B \in SubRing (S) \to S ↾_{𝑠} B \in Ring$
23		ringmgm	$⊢ S ↾_{𝑠} B \in Ring \to S ↾_{𝑠} B \in Mgm$
24	5 8 22 23	4syl	$⊢ φ \to S ↾_{𝑠} B \in Mgm$
25		simpl	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to φ$
26	1 2 3 4 5 12	ressply1bas	$⊢ φ \to B = {Base}_{(S ↾_{𝑠} B)}$
27	26	eqcomd	$⊢ φ \to {Base}_{(S ↾_{𝑠} B)} = B$
28	27	eleq2d	$⊢ φ \to (s \in {Base}_{(S ↾_{𝑠} B)} \leftrightarrow s \in B)$
29	28	biimpcd	$⊢ s \in {Base}_{(S ↾_{𝑠} B)} \to (φ \to s \in B)$
30	29	adantr	$⊢ (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)}) \to (φ \to s \in B)$
31	30	impcom	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to s \in B$
32	27	eleq2d	$⊢ φ \to (t \in {Base}_{(S ↾_{𝑠} B)} \leftrightarrow t \in B)$
33	32	biimpcd	$⊢ t \in {Base}_{(S ↾_{𝑠} B)} \to (φ \to t \in B)$
34	33	adantl	$⊢ (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)}) \to (φ \to t \in B)$
35	34	impcom	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to t \in B$
36	1 2 3 4 5 12	ressply1add	$⊢ (φ \land (s \in B \land t \in B)) \to s +_{U} t = s +_{(S ↾_{𝑠} B)} t$
37	25 31 35 36	syl12anc	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to s +_{U} t = s +_{(S ↾_{𝑠} B)} t$
38	37	eqcomd	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to s +_{(S ↾_{𝑠} B)} t = s +_{U} t$
39	7	ffund	$⊢ φ \to Fun F$
40	7	frnd	$⊢ φ \to ran F \subseteq B$
41	40 26	sseqtrd	$⊢ φ \to ran F \subseteq {Base}_{(S ↾_{𝑠} B)}$
42	14 15 17 21 24 38 39 41	gsummgmpropd	$⊢ φ \to \sum_{S ↾_{𝑠} B} F = \sum_{U} F$
43	13 42	eqtrd	$⊢ φ \to \sum_{S} F = \sum_{U} F$

Metamath Proof Explorer

Theorem gsumply1subr

Proof