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	$⊢ φ \to A \subseteq ℂ$
	fwddifval.2	$⊢ φ \to F : A ⟶ ℂ$
	fwddifval.3	$⊢ φ \to X \in A$
	fwddifval.4	$⊢ φ \to X + 1 \in A$
Assertion	fwddifval	$⊢ φ \to △ (F) (X) = F (X + 1) - F (X)$

Proof

Step	Hyp	Ref	Expression
1		fwddifval.1	$⊢ φ \to A \subseteq ℂ$
2		fwddifval.2	$⊢ φ \to F : A ⟶ ℂ$
3		fwddifval.3	$⊢ φ \to X \in A$
4		fwddifval.4	$⊢ φ \to X + 1 \in A$
5		df-fwddif	$⊢ △ = (f \in (ℂ ↑_{𝑝𝑚} ℂ) ⟼ (x \in \{y \in dom f \| y + 1 \in dom f\} ⟼ f (x + 1) - f (x)))$
6		dmeq	$⊢ f = F \to dom f = dom F$
7	6	eleq2d	$⊢ f = F \to (y + 1 \in dom f \leftrightarrow y + 1 \in dom F)$
8	6 7	rabeqbidv	$⊢ f = F \to \{y \in dom f \| y + 1 \in dom f\} = \{y \in dom F \| y + 1 \in dom F\}$
9		fveq1	$⊢ f = F \to f (x + 1) = F (x + 1)$
10		fveq1	$⊢ f = F \to f (x) = F (x)$
11	9 10	oveq12d	$⊢ f = F \to f (x + 1) - f (x) = F (x + 1) - F (x)$
12	8 11	mpteq12dv	$⊢ f = F \to (x \in \{y \in dom f \| y + 1 \in dom f\} ⟼ f (x + 1) - f (x)) = (x \in \{y \in dom F \| y + 1 \in dom F\} ⟼ F (x + 1) - F (x))$
13		cnex	$⊢ ℂ \in V$
14		elpm2r	$⊢ ((ℂ \in V \land ℂ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℂ)) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
15	13 13 14	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
16	2 1 15	syl2anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
17	2	fdmd	$⊢ φ \to dom F = A$
18	13	a1i	$⊢ φ \to ℂ \in V$
19	18 1	ssexd	$⊢ φ \to A \in V$
20	17 19	eqeltrd	$⊢ φ \to dom F \in V$
21		rabexg	$⊢ dom F \in V \to \{y \in dom F \| y + 1 \in dom F\} \in V$
22		mptexg	$⊢ \{y \in dom F \| y + 1 \in dom F\} \in V \to (x \in \{y \in dom F \| y + 1 \in dom F\} ⟼ F (x + 1) - F (x)) \in V$
23	20 21 22	3syl	$⊢ φ \to (x \in \{y \in dom F \| y + 1 \in dom F\} ⟼ F (x + 1) - F (x)) \in V$
24	5 12 16 23	fvmptd3	$⊢ φ \to △ (F) = (x \in \{y \in dom F \| y + 1 \in dom F\} ⟼ F (x + 1) - F (x))$
25	17	eleq2d	$⊢ φ \to (y + 1 \in dom F \leftrightarrow y + 1 \in A)$
26	17 25	rabeqbidv	$⊢ φ \to \{y \in dom F \| y + 1 \in dom F\} = \{y \in A \| y + 1 \in A\}$
27	26	mpteq1d	$⊢ φ \to (x \in \{y \in dom F \| y + 1 \in dom F\} ⟼ F (x + 1) - F (x)) = (x \in \{y \in A \| y + 1 \in A\} ⟼ F (x + 1) - F (x))$
28	24 27	eqtrd	$⊢ φ \to △ (F) = (x \in \{y \in A \| y + 1 \in A\} ⟼ F (x + 1) - F (x))$
29		fvoveq1	$⊢ x = X \to F (x + 1) = F (X + 1)$
30		fveq2	$⊢ x = X \to F (x) = F (X)$
31	29 30	oveq12d	$⊢ x = X \to F (x + 1) - F (x) = F (X + 1) - F (X)$
32	31	adantl	$⊢ (φ \land x = X) \to F (x + 1) - F (x) = F (X + 1) - F (X)$
33		oveq1	$⊢ y = X \to y + 1 = X + 1$
34	33	eleq1d	$⊢ y = X \to (y + 1 \in A \leftrightarrow X + 1 \in A)$
35	34	elrab	$⊢ X \in \{y \in A \| y + 1 \in A\} \leftrightarrow (X \in A \land X + 1 \in A)$
36	3 4 35	sylanbrc	$⊢ φ \to X \in \{y \in A \| y + 1 \in A\}$
37		ovexd	$⊢ φ \to F (X + 1) - F (X) \in V$
38	28 32 36 37	fvmptd	$⊢ φ \to △ (F) (X) = F (X + 1) - F (X)$

Metamath Proof Explorer

Theorem fwddifval

Proof