This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0gsumfz0

Description: Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019)

		Ref	Expression
	Hypotheses	nn0gsumfz.b	$⊢ B = {Base}_{G}$
		nn0gsumfz.0	$⊢ \underset{˙}{0} = 0_{G}$
		nn0gsumfz.g	$⊢ φ \to G \in CMnd$
		nn0gsumfz.f	$⊢ φ \to F \in (B^{ℕ_{0}})$
		nn0gsumfz.y	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	Assertion	nn0gsumfz0	$⊢ φ \to \exists s \in ℕ_{0} \exists f \in (B^{(0 \dots s)}) \sum_{G} F = \sum_{G} f$

Proof

Step	Hyp	Ref	Expression
1		nn0gsumfz.b	$⊢ B = {Base}_{G}$
2		nn0gsumfz.0	$⊢ \underset{˙}{0} = 0_{G}$
3		nn0gsumfz.g	$⊢ φ \to G \in CMnd$
4		nn0gsumfz.f	$⊢ φ \to F \in (B^{ℕ_{0}})$
5		nn0gsumfz.y	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
6	1 2 3 4 5	nn0gsumfz	$⊢ φ \to \exists s \in ℕ_{0} \exists f \in (B^{(0 \dots s)}) (f = {F ↾}_{(0 \dots s)} \land \forall x \in ℕ_{0} (s < x \to F (x) = \underset{˙}{0}) \land \sum_{G} F = \sum_{G} f)$
7		simp3	$⊢ (f = {F ↾}_{(0 \dots s)} \land \forall x \in ℕ_{0} (s < x \to F (x) = \underset{˙}{0}) \land \sum_{G} F = \sum_{G} f) \to \sum_{G} F = \sum_{G} f$
8	7	reximi	$⊢ \exists f \in (B^{(0 \dots s)}) (f = {F ↾}_{(0 \dots s)} \land \forall x \in ℕ_{0} (s < x \to F (x) = \underset{˙}{0}) \land \sum_{G} F = \sum_{G} f) \to \exists f \in (B^{(0 \dots s)}) \sum_{G} F = \sum_{G} f$
9	8	reximi	$⊢ \exists s \in ℕ_{0} \exists f \in (B^{(0 \dots s)}) (f = {F ↾}_{(0 \dots s)} \land \forall x \in ℕ_{0} (s < x \to F (x) = \underset{˙}{0}) \land \sum_{G} F = \sum_{G} f) \to \exists s \in ℕ_{0} \exists f \in (B^{(0 \dots s)}) \sum_{G} F = \sum_{G} f$
10	6 9	syl	$⊢ φ \to \exists s \in ℕ_{0} \exists f \in (B^{(0 \dots s)}) \sum_{G} F = \sum_{G} f$