Metamath Proof Explorer

Theorem fwddifval

Description: Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020)

Ref Expression
Hypotheses fwddifval.1 
|- ( ph -> A C_ CC )
fwddifval.2 
|- ( ph -> F : A --> CC )
fwddifval.3 
|- ( ph -> X e. A )
fwddifval.4 
|- ( ph -> ( X + 1 ) e. A )
Assertion fwddifval 
|- ( ph -> ( ( _/_\ ` F ) ` X ) = ( ( F ` ( X + 1 ) ) - ( F ` X ) ) )

Proof

Step Hyp Ref Expression
1 fwddifval.1 
 |-  ( ph -> A C_ CC )
2 fwddifval.2 
 |-  ( ph -> F : A --> CC )
3 fwddifval.3 
 |-  ( ph -> X e. A )
4 fwddifval.4 
 |-  ( ph -> ( X + 1 ) e. A )
5 df-fwddif 
 |-  _/_\ = ( f e. ( CC ^pm CC ) |-> ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) ) )
6 dmeq 
 |-  ( f = F -> dom f = dom F )
7 6 eleq2d 
 |-  ( f = F -> ( ( y + 1 ) e. dom f <-> ( y + 1 ) e. dom F ) )
8 6 7 rabeqbidv 
 |-  ( f = F -> { y e. dom f | ( y + 1 ) e. dom f } = { y e. dom F | ( y + 1 ) e. dom F } )
9 fveq1 
 |-  ( f = F -> ( f ` ( x + 1 ) ) = ( F ` ( x + 1 ) ) )
10 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
11 9 10 oveq12d 
 |-  ( f = F -> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) = ( ( F ` ( x + 1 ) ) - ( F ` x ) ) )
12 8 11 mpteq12dv 
 |-  ( f = F -> ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) ) = ( x e. { y e. dom F | ( y + 1 ) e. dom F } |-> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) ) )
13 cnex 
 |-  CC e. _V
14 elpm2r 
 |-  ( ( ( CC e. _V /\ CC e. _V ) /\ ( F : A --> CC /\ A C_ CC ) ) -> F e. ( CC ^pm CC ) )
15 13 13 14 mpanl12 
 |-  ( ( F : A --> CC /\ A C_ CC ) -> F e. ( CC ^pm CC ) )
16 2 1 15 syl2anc 
 |-  ( ph -> F e. ( CC ^pm CC ) )
17 2 fdmd 
 |-  ( ph -> dom F = A )
18 13 a1i 
 |-  ( ph -> CC e. _V )
19 18 1 ssexd 
 |-  ( ph -> A e. _V )
20 17 19 eqeltrd 
 |-  ( ph -> dom F e. _V )
21 rabexg 
 |-  ( dom F e. _V -> { y e. dom F | ( y + 1 ) e. dom F } e. _V )
22 mptexg 
 |-  ( { y e. dom F | ( y + 1 ) e. dom F } e. _V -> ( x e. { y e. dom F | ( y + 1 ) e. dom F } |-> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) ) e. _V )
23 20 21 22 3syl 
 |-  ( ph -> ( x e. { y e. dom F | ( y + 1 ) e. dom F } |-> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) ) e. _V )
24 5 12 16 23 fvmptd3 
 |-  ( ph -> ( _/_\ ` F ) = ( x e. { y e. dom F | ( y + 1 ) e. dom F } |-> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) ) )
25 17 eleq2d 
 |-  ( ph -> ( ( y + 1 ) e. dom F <-> ( y + 1 ) e. A ) )
26 17 25 rabeqbidv 
 |-  ( ph -> { y e. dom F | ( y + 1 ) e. dom F } = { y e. A | ( y + 1 ) e. A } )
27 26 mpteq1d 
 |-  ( ph -> ( x e. { y e. dom F | ( y + 1 ) e. dom F } |-> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) ) = ( x e. { y e. A | ( y + 1 ) e. A } |-> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) ) )
28 24 27 eqtrd 
 |-  ( ph -> ( _/_\ ` F ) = ( x e. { y e. A | ( y + 1 ) e. A } |-> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) ) )
29 fvoveq1 
 |-  ( x = X -> ( F ` ( x + 1 ) ) = ( F ` ( X + 1 ) ) )
30 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
31 29 30 oveq12d 
 |-  ( x = X -> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) = ( ( F ` ( X + 1 ) ) - ( F ` X ) ) )
32 31 adantl 
 |-  ( ( ph /\ x = X ) -> ( ( F ` ( x + 1 ) ) - ( F ` x ) ) = ( ( F ` ( X + 1 ) ) - ( F ` X ) ) )
33 oveq1 
 |-  ( y = X -> ( y + 1 ) = ( X + 1 ) )
34 33 eleq1d 
 |-  ( y = X -> ( ( y + 1 ) e. A <-> ( X + 1 ) e. A ) )
35 34 elrab 
 |-  ( X e. { y e. A | ( y + 1 ) e. A } <-> ( X e. A /\ ( X + 1 ) e. A ) )
36 3 4 35 sylanbrc 
 |-  ( ph -> X e. { y e. A | ( y + 1 ) e. A } )
37 ovexd 
 |-  ( ph -> ( ( F ` ( X + 1 ) ) - ( F ` X ) ) e. _V )
38 28 32 36 37 fvmptd 
 |-  ( ph -> ( ( _/_\ ` F ) ` X ) = ( ( F ` ( X + 1 ) ) - ( F ` X ) ) )