gsummptshft

Description: Index shift of a finite group sum over a finite set of sequential integers. (Contributed by AV, 24-Aug-2019)

	Ref	Expression
Hypotheses	gsummptshft.b	$⊢ B = {Base}_{G}$
	gsummptshft.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsummptshft.g	$⊢ φ \to G \in CMnd$
	gsummptshft.k	$⊢ φ \to K \in ℤ$
	gsummptshft.m	$⊢ φ \to M \in ℤ$
	gsummptshft.n	$⊢ φ \to N \in ℤ$
	gsummptshft.a	$⊢ (φ \land j \in (M \dots N)) \to A \in B$
	gsummptshft.c	$⊢ j = k - K \to A = C$
Assertion	gsummptshft	$⊢ φ \to {\sum_{G}}_{j = M}^{N} A = {\sum_{G}}_{k = M + K}^{N + K} C$

Proof

Step	Hyp	Ref	Expression
1		gsummptshft.b	$⊢ B = {Base}_{G}$
2		gsummptshft.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsummptshft.g	$⊢ φ \to G \in CMnd$
4		gsummptshft.k	$⊢ φ \to K \in ℤ$
5		gsummptshft.m	$⊢ φ \to M \in ℤ$
6		gsummptshft.n	$⊢ φ \to N \in ℤ$
7		gsummptshft.a	$⊢ (φ \land j \in (M \dots N)) \to A \in B$
8		gsummptshft.c	$⊢ j = k - K \to A = C$
9		ovexd	$⊢ φ \to (M \dots N) \in V$
10	7	fmpttd	$⊢ φ \to (j \in (M \dots N) ⟼ A) : (M \dots N) ⟶ B$
11		eqid	$⊢ (j \in (M \dots N) ⟼ A) = (j \in (M \dots N) ⟼ A)$
12		fzfid	$⊢ φ \to (M \dots N) \in Fin$
13	2	fvexi	$⊢ \underset{˙}{0} \in V$
14	13	a1i	$⊢ φ \to \underset{˙}{0} \in V$
15	11 12 7 14	fsuppmptdm	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((j \in (M \dots N) ⟼ A))$
16	4 5 6	mptfzshft	$⊢ φ \to (k \in (M + K \dots N + K) ⟼ k - K) : (M + K \dots N + K) \underset{1-1 onto}{⟶} (M \dots N)$
17	1 2 3 9 10 15 16	gsumf1o	$⊢ φ \to {\sum_{G}}_{j = M}^{N} A = \sum_{G} ((j \in (M \dots N) ⟼ A) \circ (k \in (M + K \dots N + K) ⟼ k - K))$
18		elfzelz	$⊢ k \in (M + K \dots N + K) \to k \in ℤ$
19	18	zcnd	$⊢ k \in (M + K \dots N + K) \to k \in ℂ$
20	4	zcnd	$⊢ φ \to K \in ℂ$
21		npcan	$⊢ (k \in ℂ \land K \in ℂ) \to k - K + K = k$
22	19 20 21	syl2anr	$⊢ (φ \land k \in (M + K \dots N + K)) \to k - K + K = k$
23		simpr	$⊢ (φ \land k \in (M + K \dots N + K)) \to k \in (M + K \dots N + K)$
24	22 23	eqeltrd	$⊢ (φ \land k \in (M + K \dots N + K)) \to k - K + K \in (M + K \dots N + K)$
25	5 6	jca	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
26	25	adantr	$⊢ (φ \land k \in (M + K \dots N + K)) \to (M \in ℤ \land N \in ℤ)$
27	18	adantl	$⊢ (φ \land k \in (M + K \dots N + K)) \to k \in ℤ$
28	4	adantr	$⊢ (φ \land k \in (M + K \dots N + K)) \to K \in ℤ$
29	27 28	zsubcld	$⊢ (φ \land k \in (M + K \dots N + K)) \to k - K \in ℤ$
30		fzaddel	$⊢ ((M \in ℤ \land N \in ℤ) \land (k - K \in ℤ \land K \in ℤ)) \to (k - K \in (M \dots N) \leftrightarrow k - K + K \in (M + K \dots N + K))$
31	26 29 28 30	syl12anc	$⊢ (φ \land k \in (M + K \dots N + K)) \to (k - K \in (M \dots N) \leftrightarrow k - K + K \in (M + K \dots N + K))$
32	24 31	mpbird	$⊢ (φ \land k \in (M + K \dots N + K)) \to k - K \in (M \dots N)$
33		eqidd	$⊢ φ \to (k \in (M + K \dots N + K) ⟼ k - K) = (k \in (M + K \dots N + K) ⟼ k - K)$
34		eqidd	$⊢ φ \to (j \in (M \dots N) ⟼ A) = (j \in (M \dots N) ⟼ A)$
35	32 33 34 8	fmptco	$⊢ φ \to (j \in (M \dots N) ⟼ A) \circ (k \in (M + K \dots N + K) ⟼ k - K) = (k \in (M + K \dots N + K) ⟼ C)$
36	35	oveq2d	$⊢ φ \to \sum_{G} ((j \in (M \dots N) ⟼ A) \circ (k \in (M + K \dots N + K) ⟼ k - K)) = {\sum_{G}}_{k = M + K}^{N + K} C$
37	17 36	eqtrd	$⊢ φ \to {\sum_{G}}_{j = M}^{N} A = {\sum_{G}}_{k = M + K}^{N + K} C$

Metamath Proof Explorer

Theorem gsummptshft

Proof