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	9 10	syl	$⊢ B \in SubRing (S) \to B \in SubMnd (S)$
12	5 8 11	3syl	$⊢ φ \to B \in SubMnd (S)$
13		eqid	$⊢ S ↾_{𝑠} B = S ↾_{𝑠} B$
14	6 12 7 13	gsumsubm	$⊢ φ \to \sum_{S} F = \sum_{S ↾_{𝑠} B} F$
15		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
16	7 6 15	syl2anc	$⊢ φ \to F \in V$
17		ovexd	$⊢ φ \to S ↾_{𝑠} B \in V$
18	3	fvexi	$⊢ U \in V$
19	18	a1i	$⊢ φ \to U \in V$
20		eqid	$⊢ {Base}_{U} = {Base}_{U}$
21	4	oveq2i	$⊢ S ↾_{𝑠} B = S ↾_{𝑠} {Base}_{U}$
22	1 2 3 20 5 21	ressply1bas	$⊢ φ \to {Base}_{U} = {Base}_{(S ↾_{𝑠} B)}$
23	22	eqcomd	$⊢ φ \to {Base}_{(S ↾_{𝑠} B)} = {Base}_{U}$
24	13	subrgring	$⊢ B \in SubRing (S) \to S ↾_{𝑠} B \in Ring$
25	8 24	syl	$⊢ T \in SubRing (R) \to S ↾_{𝑠} B \in Ring$
26		ringmgm	$⊢ S ↾_{𝑠} B \in Ring \to S ↾_{𝑠} B \in Mgm$
27	5 25 26	3syl	$⊢ φ \to S ↾_{𝑠} B \in Mgm$
28		simpl	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to φ$
29	1 2 3 4 5 13	ressply1bas	$⊢ φ \to B = {Base}_{(S ↾_{𝑠} B)}$
30	29	eqcomd	$⊢ φ \to {Base}_{(S ↾_{𝑠} B)} = B$
31	30	eleq2d	$⊢ φ \to (s \in {Base}_{(S ↾_{𝑠} B)} \leftrightarrow s \in B)$
32	31	biimpcd	$⊢ s \in {Base}_{(S ↾_{𝑠} B)} \to (φ \to s \in B)$
33	32	adantr	$⊢ (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)}) \to (φ \to s \in B)$
34	33	impcom	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to s \in B$
35	30	eleq2d	$⊢ φ \to (t \in {Base}_{(S ↾_{𝑠} B)} \leftrightarrow t \in B)$
36	35	biimpcd	$⊢ t \in {Base}_{(S ↾_{𝑠} B)} \to (φ \to t \in B)$
37	36	adantl	$⊢ (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)}) \to (φ \to t \in B)$
38	37	impcom	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to t \in B$
39	1 2 3 4 5 13	ressply1add	$⊢ (φ \land (s \in B \land t \in B)) \to s +_{U} t = s +_{(S ↾_{𝑠} B)} t$
40	28 34 38 39	syl12anc	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to s +_{U} t = s +_{(S ↾_{𝑠} B)} t$
41	40	eqcomd	$⊢ (φ \land (s \in {Base}_{(S ↾_{𝑠} B)} \land t \in {Base}_{(S ↾_{𝑠} B)})) \to s +_{(S ↾_{𝑠} B)} t = s +_{U} t$
42	7	ffund	$⊢ φ \to Fun F$
43	7	frnd	$⊢ φ \to ran F \subseteq B$
44	43 29	sseqtrd	$⊢ φ \to ran F \subseteq {Base}_{(S ↾_{𝑠} B)}$
45	16 17 19 23 27 41 42 44	gsummgmpropd	$⊢ φ \to \sum_{S ↾_{𝑠} B} F = \sum_{U} F$
46	14 45	eqtrd	$⊢ φ \to \sum_{S} F = \sum_{U} F$

Metamath Proof Explorer

Theorem gsumply1subr

Proof