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	\|- ( ph -> N e. ( ZZ>= ` M ) )
	seqfeq4.f	\|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
	seqfeq4.cl	\|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
	seqfeq4.id	\|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( x Q y ) )
Assertion	seqfeq4	\|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq M ( Q , F ) ` N ) )

Proof

Step	Hyp	Ref	Expression
1		seqfeq4.m	\|- ( ph -> N e. ( ZZ>= ` M ) )
2		seqfeq4.f	\|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
3		seqfeq4.cl	\|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
4		seqfeq4.id	\|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( x Q y ) )
5		fvex	\|- ( seq M ( .+ , F ) ` N ) e. _V
6		fvi	\|- ( ( seq M ( .+ , F ) ` N ) e. _V -> ( _I ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( .+ , F ) ` N ) )
7	5 6	ax-mp	\|- ( _I ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( .+ , F ) ` N )
8		ovex	\|- ( x .+ y ) e. _V
9		fvi	\|- ( ( x .+ y ) e. _V -> ( _I ` ( x .+ y ) ) = ( x .+ y ) )
10	8 9	ax-mp	\|- ( _I ` ( x .+ y ) ) = ( x .+ y )
11		fvi	\|- ( x e. _V -> ( _I ` x ) = x )
12	11	elv	\|- ( _I ` x ) = x
13		fvi	\|- ( y e. _V -> ( _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	\|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( _I ` ( x .+ y ) ) = ( ( _I ` x ) Q ( _I ` y ) ) )
17		fvex	\|- ( F ` x ) e. _V
18		fvi	\|- ( ( F ` x ) e. _V -> ( _I ` ( F ` x ) ) = ( F ` x ) )
19	17 18	mp1i	\|- ( ( ph /\ x e. ( M ... N ) ) -> ( _I ` ( F ` x ) ) = ( F ` x ) )
20	3 2 1 16 19	seqhomo	\|- ( ph -> ( _I ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , F ) ` N ) )
21	7 20	eqtr3id	\|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq M ( Q , F ) ` N ) )

Metamath Proof Explorer

Theorem seqfeq4

Proof