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

Metamath Proof Explorer

Theorem gsumply1subr

Proof