Theorem 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	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	seqfeq4.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
	seqfeq4.cl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
	seqfeq4.id	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 𝑄 𝑦 ) )
Assertion	seqfeq4	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( 𝑄 , 𝐹 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		seqfeq4.m	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		seqfeq4.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
3		seqfeq4.cl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4		seqfeq4.id	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 𝑄 𝑦 ) )
5		fvex	⊢ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V
6		fvi	⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V → ( I ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
7	5 6	ax-mp	⊢ ( I ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 )
8		ovex	⊢ ( 𝑥 + 𝑦 ) ∈ V
9		fvi	⊢ ( ( 𝑥 + 𝑦 ) ∈ V → ( I ‘ ( 𝑥 + 𝑦 ) ) = ( 𝑥 + 𝑦 ) )
10	8 9	ax-mp	⊢ ( I ‘ ( 𝑥 + 𝑦 ) ) = ( 𝑥 + 𝑦 )
11		fvi	⊢ ( 𝑥 ∈ V → ( I ‘ 𝑥 ) = 𝑥 )
12	11	elv	⊢ ( I ‘ 𝑥 ) = 𝑥
13		fvi	⊢ ( 𝑦 ∈ V → ( I ‘ 𝑦 ) = 𝑦 )
14	13	elv	⊢ ( I ‘ 𝑦 ) = 𝑦
15	12 14	oveq12i	⊢ ( ( I ‘ 𝑥 ) 𝑄 ( I ‘ 𝑦 ) ) = ( 𝑥 𝑄 𝑦 )
16	4 10 15	3eqtr4g	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( I ‘ ( 𝑥 + 𝑦 ) ) = ( ( I ‘ 𝑥 ) 𝑄 ( I ‘ 𝑦 ) ) )
17		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
18		fvi	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ V → ( I ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
19	17 18	mp1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( I ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
20	3 2 1 16 19	seqhomo	⊢ ( 𝜑 → ( I ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐹 ) ‘ 𝑁 ) )
21	7 20	eqtr3id	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( 𝑄 , 𝐹 ) ‘ 𝑁 ) )