Step |
Hyp |
Ref |
Expression |
1 |
|
dvres.k |
|- K = ( TopOpen ` CCfld ) |
2 |
|
dvres.t |
|- T = ( K |`t S ) |
3 |
|
reldv |
|- Rel ( S _D ( F |` B ) ) |
4 |
|
relres |
|- Rel ( ( S _D F ) |` ( ( int ` T ) ` B ) ) |
5 |
|
simpll |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> S C_ CC ) |
6 |
|
simplr |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> F : A --> CC ) |
7 |
|
inss1 |
|- ( A i^i B ) C_ A |
8 |
|
fssres |
|- ( ( F : A --> CC /\ ( A i^i B ) C_ A ) -> ( F |` ( A i^i B ) ) : ( A i^i B ) --> CC ) |
9 |
6 7 8
|
sylancl |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( F |` ( A i^i B ) ) : ( A i^i B ) --> CC ) |
10 |
|
resres |
|- ( ( F |` A ) |` B ) = ( F |` ( A i^i B ) ) |
11 |
|
ffn |
|- ( F : A --> CC -> F Fn A ) |
12 |
|
fnresdm |
|- ( F Fn A -> ( F |` A ) = F ) |
13 |
6 11 12
|
3syl |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( F |` A ) = F ) |
14 |
13
|
reseq1d |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( F |` A ) |` B ) = ( F |` B ) ) |
15 |
10 14
|
syl5eqr |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( F |` ( A i^i B ) ) = ( F |` B ) ) |
16 |
15
|
feq1d |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( F |` ( A i^i B ) ) : ( A i^i B ) --> CC <-> ( F |` B ) : ( A i^i B ) --> CC ) ) |
17 |
9 16
|
mpbid |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( F |` B ) : ( A i^i B ) --> CC ) |
18 |
|
simprl |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> A C_ S ) |
19 |
7 18
|
sstrid |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( A i^i B ) C_ S ) |
20 |
5 17 19
|
dvcl |
|- ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ x ( S _D ( F |` B ) ) y ) -> y e. CC ) |
21 |
20
|
ex |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( x ( S _D ( F |` B ) ) y -> y e. CC ) ) |
22 |
5 6 18
|
dvcl |
|- ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ x ( S _D F ) y ) -> y e. CC ) |
23 |
22
|
ex |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( x ( S _D F ) y -> y e. CC ) ) |
24 |
23
|
adantld |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) -> y e. CC ) ) |
25 |
|
eqid |
|- ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) |
26 |
5
|
adantr |
|- ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> S C_ CC ) |
27 |
6
|
adantr |
|- ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> F : A --> CC ) |
28 |
18
|
adantr |
|- ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> A C_ S ) |
29 |
|
simplrr |
|- ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> B C_ S ) |
30 |
|
simpr |
|- ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> y e. CC ) |
31 |
1 2 25 26 27 28 29 30
|
dvreslem |
|- ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) ) ) |
32 |
31
|
ex |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( y e. CC -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) ) ) ) |
33 |
21 24 32
|
pm5.21ndd |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) ) ) |
34 |
|
vex |
|- y e. _V |
35 |
34
|
brresi |
|- ( x ( ( S _D F ) |` ( ( int ` T ) ` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) ) |
36 |
33 35
|
bitr4di |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( x ( S _D ( F |` B ) ) y <-> x ( ( S _D F ) |` ( ( int ` T ) ` B ) ) y ) ) |
37 |
3 4 36
|
eqbrrdiv |
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( S _D ( F |` B ) ) = ( ( S _D F ) |` ( ( int ` T ) ` B ) ) ) |