Metamath Proof Explorer

Theorem vdwapval

Description: Value of the arithmetic progression function. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Assertion vdwapval 
|- ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( X e. ( A ( AP ` K ) D ) <-> E. m e. ( 0 ... ( K - 1 ) ) X = ( A + ( m x. D ) ) ) )

Proof

Step Hyp Ref Expression
1 vdwapfval 
 |-  ( K e. NN0 -> ( AP ` K ) = ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
2 1 3ad2ant1 
 |-  ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( AP ` K ) = ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
3 2 oveqd 
 |-  ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( AP ` K ) D ) = ( A ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) D ) )
4 oveq2 
 |-  ( d = D -> ( m x. d ) = ( m x. D ) )
5 oveq12 
 |-  ( ( a = A /\ ( m x. d ) = ( m x. D ) ) -> ( a + ( m x. d ) ) = ( A + ( m x. D ) ) )
6 4 5 sylan2 
 |-  ( ( a = A /\ d = D ) -> ( a + ( m x. d ) ) = ( A + ( m x. D ) ) )
7 6 mpteq2dv 
 |-  ( ( a = A /\ d = D ) -> ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) = ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) )
8 7 rneqd 
 |-  ( ( a = A /\ d = D ) -> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) = ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) )
9 eqid 
 |-  ( 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 ) ) ) )
10 ovex 
 |-  ( 0 ... ( K - 1 ) ) e. _V
11 10 mptex 
 |-  ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) e. _V
12 11 rnex 
 |-  ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) e. _V
13 8 9 12 ovmpoa 
 |-  ( ( A e. NN /\ D e. NN ) -> ( A ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) D ) = ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) )
14 13 3adant1 
 |-  ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( a + ( m x. d ) ) ) ) D ) = ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) )
15 3 14 eqtrd 
 |-  ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( AP ` K ) D ) = ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) )
16 eqid 
 |-  ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) = ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) )
17 16 rnmpt 
 |-  ran ( m e. ( 0 ... ( K - 1 ) ) |-> ( A + ( m x. D ) ) ) = { x | E. m e. ( 0 ... ( K - 1 ) ) x = ( A + ( m x. D ) ) }
18 15 17 eqtrdi 
 |-  ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( AP ` K ) D ) = { x | E. m e. ( 0 ... ( K - 1 ) ) x = ( A + ( m x. D ) ) } )
19 18 eleq2d 
 |-  ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( X e. ( A ( AP ` K ) D ) <-> X e. { x | E. m e. ( 0 ... ( K - 1 ) ) x = ( A + ( m x. D ) ) } ) )
20 id 
 |-  ( X = ( A + ( m x. D ) ) -> X = ( A + ( m x. D ) ) )
21 ovex 
 |-  ( A + ( m x. D ) ) e. _V
22 20 21 eqeltrdi 
 |-  ( X = ( A + ( m x. D ) ) -> X e. _V )
23 22 rexlimivw 
 |-  ( E. m e. ( 0 ... ( K - 1 ) ) X = ( A + ( m x. D ) ) -> X e. _V )
24 eqeq1 
 |-  ( x = X -> ( x = ( A + ( m x. D ) ) <-> X = ( A + ( m x. D ) ) ) )
25 24 rexbidv 
 |-  ( x = X -> ( E. m e. ( 0 ... ( K - 1 ) ) x = ( A + ( m x. D ) ) <-> E. m e. ( 0 ... ( K - 1 ) ) X = ( A + ( m x. D ) ) ) )
26 23 25 elab3 
 |-  ( X e. { x | E. m e. ( 0 ... ( K - 1 ) ) x = ( A + ( m x. D ) ) } <-> E. m e. ( 0 ... ( K - 1 ) ) X = ( A + ( m x. D ) ) )
27 19 26 bitrdi 
 |-  ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( X e. ( A ( AP ` K ) D ) <-> E. m e. ( 0 ... ( K - 1 ) ) X = ( A + ( m x. D ) ) ) )