Metamath Proof Explorer

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 
|- ( K e. NN0 -> ( AP ` K ) = ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( k = K /\ a e. NN /\ d e. NN ) -> k = K )
2 1 oveq1d 
 |-  ( ( k = K /\ a e. NN /\ d e. NN ) -> ( k - 1 ) = ( K - 1 ) )
3 2 oveq2d 
 |-  ( ( k = K /\ a e. NN /\ d e. NN ) -> ( 0 ... ( k - 1 ) ) = ( 0 ... ( K - 1 ) ) )
4 3 mpteq1d 
 |-  ( ( k = K /\ a e. NN /\ d e. NN ) -> ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) = ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) )
5 4 rneqd 
 |-  ( ( k = K /\ a e. NN /\ d e. NN ) -> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) = ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) )
6 5 mpoeq3dva 
 |-  ( k = K -> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) = ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
7 df-vdwap 
 |-  AP = ( k e. NN0 |-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
8 nnex 
 |-  NN e. _V
9 8 8 mpoex 
 |-  ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) e. _V
10 6 7 9 fvmpt 
 |-  ( K e. NN0 -> ( AP ` K ) = ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )