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