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	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	fwddifval.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	fwddifval.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	fwddifval.4	⊢ ( 𝜑 → ( 𝑋 + 1 ) ∈ 𝐴 )
Assertion	fwddifval	⊢ ( 𝜑 → ( ( △ ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ ( 𝑋 + 1 ) ) − ( 𝐹 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fwddifval.1	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2		fwddifval.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		fwddifval.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4		fwddifval.4	⊢ ( 𝜑 → ( 𝑋 + 1 ) ∈ 𝐴 )
5		df-fwddif	⊢ △ = ( 𝑓 ∈ ( ℂ ↑pm ℂ ) ↦ ( 𝑥 ∈ { 𝑦 ∈ dom 𝑓 ∣ ( 𝑦 + 1 ) ∈ dom 𝑓 } ↦ ( ( 𝑓 ‘ ( 𝑥 + 1 ) ) − ( 𝑓 ‘ 𝑥 ) ) ) )
6		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
7	6	eleq2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑦 + 1 ) ∈ dom 𝑓 ↔ ( 𝑦 + 1 ) ∈ dom 𝐹 ) )
8	6 7	rabeqbidv	⊢ ( 𝑓 = 𝐹 → { 𝑦 ∈ dom 𝑓 ∣ ( 𝑦 + 1 ) ∈ dom 𝑓 } = { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } )
9		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 + 1 ) ) = ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
10		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
11	9 10	oveq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 + 1 ) ) − ( 𝑓 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) )
12	8 11	mpteq12dv	⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ { 𝑦 ∈ dom 𝑓 ∣ ( 𝑦 + 1 ) ∈ dom 𝑓 } ↦ ( ( 𝑓 ‘ ( 𝑥 + 1 ) ) − ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } ↦ ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) ) )
13		cnex	⊢ ℂ ∈ V
14		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ) ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
15	13 13 14	mpanl12	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
16	2 1 15	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
17	2	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
18	13	a1i	⊢ ( 𝜑 → ℂ ∈ V )
19	18 1	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
20	17 19	eqeltrd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
21		rabexg	⊢ ( dom 𝐹 ∈ V → { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } ∈ V )
22		mptexg	⊢ ( { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } ∈ V → ( 𝑥 ∈ { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } ↦ ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) ) ∈ V )
23	20 21 22	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } ↦ ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) ) ∈ V )
24	5 12 16 23	fvmptd3	⊢ ( 𝜑 → ( △ ‘ 𝐹 ) = ( 𝑥 ∈ { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } ↦ ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) ) )
25	17	eleq2d	⊢ ( 𝜑 → ( ( 𝑦 + 1 ) ∈ dom 𝐹 ↔ ( 𝑦 + 1 ) ∈ 𝐴 ) )
26	17 25	rabeqbidv	⊢ ( 𝜑 → { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } = { 𝑦 ∈ 𝐴 ∣ ( 𝑦 + 1 ) ∈ 𝐴 } )
27	26	mpteq1d	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ dom 𝐹 ∣ ( 𝑦 + 1 ) ∈ dom 𝐹 } ↦ ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ ( 𝑦 + 1 ) ∈ 𝐴 } ↦ ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) ) )
28	24 27	eqtrd	⊢ ( 𝜑 → ( △ ‘ 𝐹 ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ ( 𝑦 + 1 ) ∈ 𝐴 } ↦ ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) ) )
29		fvoveq1	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 𝑥 + 1 ) ) = ( 𝐹 ‘ ( 𝑋 + 1 ) ) )
30		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
31	29 30	oveq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 1 ) ) − ( 𝐹 ‘ 𝑋 ) ) )
32	31	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝐹 ‘ ( 𝑥 + 1 ) ) − ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 1 ) ) − ( 𝐹 ‘ 𝑋 ) ) )
33		oveq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 + 1 ) = ( 𝑋 + 1 ) )
34	33	eleq1d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 + 1 ) ∈ 𝐴 ↔ ( 𝑋 + 1 ) ∈ 𝐴 ) )
35	34	elrab	⊢ ( 𝑋 ∈ { 𝑦 ∈ 𝐴 ∣ ( 𝑦 + 1 ) ∈ 𝐴 } ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝑋 + 1 ) ∈ 𝐴 ) )
36	3 4 35	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ { 𝑦 ∈ 𝐴 ∣ ( 𝑦 + 1 ) ∈ 𝐴 } )
37		ovexd	⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑋 + 1 ) ) − ( 𝐹 ‘ 𝑋 ) ) ∈ V )
38	28 32 36 37	fvmptd	⊢ ( 𝜑 → ( ( △ ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ ( 𝑋 + 1 ) ) − ( 𝐹 ‘ 𝑋 ) ) )