Theorem vdwapfval

Description: Define the arithmetic progression function, which takes as input a length k , a start point a , and a step d and outputs the set of points in this progression. (Contributed by Mario Carneiro, 18-Aug-2014)

	Ref	Expression
Assertion	vdwapfval	⊢ ( 𝐾 ∈ ℕ0 → ( AP ‘ 𝐾 ) = ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → 𝑘 = 𝐾 )
2	1	oveq1d	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 𝑘 − 1 ) = ( 𝐾 − 1 ) )
3	2	oveq2d	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 0 ... ( 𝑘 − 1 ) ) = ( 0 ... ( 𝐾 − 1 ) ) )
4	3	mpteq1d	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) )
5	4	rneqd	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ran ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) )
6	5	mpoeq3dva	⊢ ( 𝑘 = 𝐾 → ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) = ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )
7		df-vdwap	⊢ AP = ( 𝑘 ∈ ℕ0 ↦ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )
8		nnex	⊢ ℕ ∈ V
9	8 8	mpoex	⊢ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) ∈ V
10	6 7 9	fvmpt	⊢ ( 𝐾 ∈ ℕ0 → ( AP ‘ 𝐾 ) = ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )