seqfeq4

Description: Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	seqfeq4.m	$⊢ φ \to N \in ℤ_{\geq M}$
	seqfeq4.f	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
	seqfeq4.cl	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqfeq4.id	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y = x Q y$
Assertion	seqfeq4	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq M (Q, F) (N)$

Proof

Step	Hyp	Ref	Expression
1		seqfeq4.m	$⊢ φ \to N \in ℤ_{\geq M}$
2		seqfeq4.f	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
3		seqfeq4.cl	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
4		seqfeq4.id	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y = x Q y$
5		fvex	$⊢ seq M (\underset{˙}{+}, F) (N) \in V$
6		fvi	$⊢ seq M (\underset{˙}{+}, F) (N) \in V \to I (seq M (\underset{˙}{+}, F) (N)) = seq M (\underset{˙}{+}, F) (N)$
7	5 6	ax-mp	$⊢ I (seq M (\underset{˙}{+}, F) (N)) = seq M (\underset{˙}{+}, F) (N)$
8		ovex	$⊢ x \underset{˙}{+} y \in V$
9		fvi	$⊢ x \underset{˙}{+} y \in V \to I (x \underset{˙}{+} y) = x \underset{˙}{+} y$
10	8 9	ax-mp	$⊢ I (x \underset{˙}{+} y) = x \underset{˙}{+} y$
11		fvi	$⊢ x \in V \to I (x) = x$
12	11	elv	$⊢ I (x) = x$
13		fvi	$⊢ y \in V \to I (y) = y$
14	13	elv	$⊢ I (y) = y$
15	12 14	oveq12i	$⊢ I (x) Q I (y) = x Q y$
16	4 10 15	3eqtr4g	$⊢ (φ \land (x \in S \land y \in S)) \to I (x \underset{˙}{+} y) = I (x) Q I (y)$
17		fvex	$⊢ F (x) \in V$
18		fvi	$⊢ F (x) \in V \to I (F (x)) = F (x)$
19	17 18	mp1i	$⊢ (φ \land x \in (M \dots N)) \to I (F (x)) = F (x)$
20	3 2 1 16 19	seqhomo	$⊢ φ \to I (seq M (\underset{˙}{+}, F) (N)) = seq M (Q, F) (N)$
21	7 20	eqtr3id	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq M (Q, F) (N)$

Metamath Proof Explorer

Theorem seqfeq4

Proof