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 φ A
fwddifval.2 φ F : A
fwddifval.3 φ X A
fwddifval.4 φ X + 1 A
Assertion fwddifval φ F X = F X + 1 F X

Proof

Step Hyp Ref Expression
1 fwddifval.1 φ A
2 fwddifval.2 φ F : A
3 fwddifval.3 φ X A
4 fwddifval.4 φ X + 1 A
5 df-fwddif = f 𝑝𝑚 x y dom f | y + 1 dom f f x + 1 f x
6 dmeq f = F dom f = dom F
7 6 eleq2d f = F y + 1 dom f y + 1 dom F
8 6 7 rabeqbidv f = F y dom f | y + 1 dom f = y dom F | y + 1 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 y dom f | y + 1 dom f f x + 1 f x = x y dom F | y + 1 dom F F x + 1 F x
13 cnex V
14 elpm2r V V F : A A F 𝑝𝑚
15 13 13 14 mpanl12 F : A A F 𝑝𝑚
16 2 1 15 syl2anc φ F 𝑝𝑚
17 2 fdmd φ dom F = A
18 13 a1i φ V
19 18 1 ssexd φ A V
20 17 19 eqeltrd φ dom F V
21 rabexg dom F V y dom F | y + 1 dom F V
22 mptexg y dom F | y + 1 dom F V x y dom F | y + 1 dom F F x + 1 F x V
23 20 21 22 3syl φ x y dom F | y + 1 dom F F x + 1 F x V
24 5 12 16 23 fvmptd3 φ F = x y dom F | y + 1 dom F F x + 1 F x
25 17 eleq2d φ y + 1 dom F y + 1 A
26 17 25 rabeqbidv φ y dom F | y + 1 dom F = y A | y + 1 A
27 26 mpteq1d φ x y dom F | y + 1 dom F F x + 1 F x = x y A | y + 1 A F x + 1 F x
28 24 27 eqtrd φ F = x y A | y + 1 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 φ 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 A X + 1 A
35 34 elrab X y A | y + 1 A X A X + 1 A
36 3 4 35 sylanbrc φ X y A | y + 1 A
37 ovexd φ F X + 1 F X V
38 28 32 36 37 fvmptd φ F X = F X + 1 F X