Metamath Proof Explorer


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
|- ( 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 ) )