Step |
Hyp |
Ref |
Expression |
1 |
|
shftfval.1 |
|- F e. _V |
2 |
|
ffn |
|- ( F : B --> C -> F Fn B ) |
3 |
1
|
shftfn |
|- ( ( F Fn B /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } ) |
4 |
2 3
|
sylan |
|- ( ( F : B --> C /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } ) |
5 |
|
oveq1 |
|- ( x = y -> ( x - A ) = ( y - A ) ) |
6 |
5
|
eleq1d |
|- ( x = y -> ( ( x - A ) e. B <-> ( y - A ) e. B ) ) |
7 |
6
|
elrab |
|- ( y e. { x e. CC | ( x - A ) e. B } <-> ( y e. CC /\ ( y - A ) e. B ) ) |
8 |
|
simpr |
|- ( ( F : B --> C /\ A e. CC ) -> A e. CC ) |
9 |
|
simpl |
|- ( ( y e. CC /\ ( y - A ) e. B ) -> y e. CC ) |
10 |
1
|
shftval |
|- ( ( A e. CC /\ y e. CC ) -> ( ( F shift A ) ` y ) = ( F ` ( y - A ) ) ) |
11 |
8 9 10
|
syl2an |
|- ( ( ( F : B --> C /\ A e. CC ) /\ ( y e. CC /\ ( y - A ) e. B ) ) -> ( ( F shift A ) ` y ) = ( F ` ( y - A ) ) ) |
12 |
|
simpl |
|- ( ( F : B --> C /\ A e. CC ) -> F : B --> C ) |
13 |
|
simpr |
|- ( ( y e. CC /\ ( y - A ) e. B ) -> ( y - A ) e. B ) |
14 |
|
ffvelrn |
|- ( ( F : B --> C /\ ( y - A ) e. B ) -> ( F ` ( y - A ) ) e. C ) |
15 |
12 13 14
|
syl2an |
|- ( ( ( F : B --> C /\ A e. CC ) /\ ( y e. CC /\ ( y - A ) e. B ) ) -> ( F ` ( y - A ) ) e. C ) |
16 |
11 15
|
eqeltrd |
|- ( ( ( F : B --> C /\ A e. CC ) /\ ( y e. CC /\ ( y - A ) e. B ) ) -> ( ( F shift A ) ` y ) e. C ) |
17 |
7 16
|
sylan2b |
|- ( ( ( F : B --> C /\ A e. CC ) /\ y e. { x e. CC | ( x - A ) e. B } ) -> ( ( F shift A ) ` y ) e. C ) |
18 |
17
|
ralrimiva |
|- ( ( F : B --> C /\ A e. CC ) -> A. y e. { x e. CC | ( x - A ) e. B } ( ( F shift A ) ` y ) e. C ) |
19 |
|
ffnfv |
|- ( ( F shift A ) : { x e. CC | ( x - A ) e. B } --> C <-> ( ( F shift A ) Fn { x e. CC | ( x - A ) e. B } /\ A. y e. { x e. CC | ( x - A ) e. B } ( ( F shift A ) ` y ) e. C ) ) |
20 |
4 18 19
|
sylanbrc |
|- ( ( F : B --> C /\ A e. CC ) -> ( F shift A ) : { x e. CC | ( x - A ) e. B } --> C ) |