Metamath Proof Explorer

Theorem vdwmc2

Description: Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdwmc.1 
|- X e. _V
vdwmc.2 
|- ( ph -> K e. NN0 )
vdwmc.3 
|- ( ph -> F : X --> R )
vdwmc2.4 
|- ( ph -> A e. X )
Assertion vdwmc2 
|- ( ph -> ( K MonoAP F <-> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )

Proof

Step Hyp Ref Expression
1 vdwmc.1 
 |-  X e. _V
2 vdwmc.2 
 |-  ( ph -> K e. NN0 )
3 vdwmc.3 
 |-  ( ph -> F : X --> R )
4 vdwmc2.4 
 |-  ( ph -> A e. X )
5 1 2 3 vdwmc 
 |-  ( ph -> ( K MonoAP F <-> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
6 vdwapid1 
 |-  ( ( K e. NN /\ a e. NN /\ d e. NN ) -> a e. ( a ( AP ` K ) d ) )
7 6 ne0d 
 |-  ( ( K e. NN /\ a e. NN /\ d e. NN ) -> ( a ( AP ` K ) d ) =/= (/) )
8 7 3expb 
 |-  ( ( K e. NN /\ ( a e. NN /\ d e. NN ) ) -> ( a ( AP ` K ) d ) =/= (/) )
9 8 adantll 
 |-  ( ( ( ph /\ K e. NN ) /\ ( a e. NN /\ d e. NN ) ) -> ( a ( AP ` K ) d ) =/= (/) )
10 ssn0 
 |-  ( ( ( a ( AP ` K ) d ) C_ ( `' F " { c } ) /\ ( a ( AP ` K ) d ) =/= (/) ) -> ( `' F " { c } ) =/= (/) )
11 10 expcom 
 |-  ( ( a ( AP ` K ) d ) =/= (/) -> ( ( a ( AP ` K ) d ) C_ ( `' F " { c } ) -> ( `' F " { c } ) =/= (/) ) )
12 9 11 syl 
 |-  ( ( ( ph /\ K e. NN ) /\ ( a e. NN /\ d e. NN ) ) -> ( ( a ( AP ` K ) d ) C_ ( `' F " { c } ) -> ( `' F " { c } ) =/= (/) ) )
13 disjsn 
 |-  ( ( R i^i { c } ) = (/) <-> -. c e. R )
14 3 adantr 
 |-  ( ( ph /\ K e. NN ) -> F : X --> R )
15 fimacnvdisj 
 |-  ( ( F : X --> R /\ ( R i^i { c } ) = (/) ) -> ( `' F " { c } ) = (/) )
16 15 ex 
 |-  ( F : X --> R -> ( ( R i^i { c } ) = (/) -> ( `' F " { c } ) = (/) ) )
17 14 16 syl 
 |-  ( ( ph /\ K e. NN ) -> ( ( R i^i { c } ) = (/) -> ( `' F " { c } ) = (/) ) )
18 17 adantr 
 |-  ( ( ( ph /\ K e. NN ) /\ ( a e. NN /\ d e. NN ) ) -> ( ( R i^i { c } ) = (/) -> ( `' F " { c } ) = (/) ) )
19 13 18 biimtrrid 
 |-  ( ( ( ph /\ K e. NN ) /\ ( a e. NN /\ d e. NN ) ) -> ( -. c e. R -> ( `' F " { c } ) = (/) ) )
20 19 necon1ad 
 |-  ( ( ( ph /\ K e. NN ) /\ ( a e. NN /\ d e. NN ) ) -> ( ( `' F " { c } ) =/= (/) -> c e. R ) )
21 12 20 syld 
 |-  ( ( ( ph /\ K e. NN ) /\ ( a e. NN /\ d e. NN ) ) -> ( ( a ( AP ` K ) d ) C_ ( `' F " { c } ) -> c e. R ) )
22 21 rexlimdvva 
 |-  ( ( ph /\ K e. NN ) -> ( E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) -> c e. R ) )
23 22 pm4.71rd 
 |-  ( ( ph /\ K e. NN ) -> ( E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> ( c e. R /\ E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) ) )
24 23 exbidv 
 |-  ( ( ph /\ K e. NN ) -> ( E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> E. c ( c e. R /\ E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) ) )
25 df-rex 
 |-  ( E. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> E. c ( c e. R /\ E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
26 24 25 bitr4di 
 |-  ( ( ph /\ K e. NN ) -> ( E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> E. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
27 3 4 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. R )
28 27 ne0d 
 |-  ( ph -> R =/= (/) )
29 1nn 
 |-  1 e. NN
30 29 ne0ii 
 |-  NN =/= (/)
31 simpllr 
 |-  ( ( ( ( ph /\ K = 0 ) /\ a e. NN ) /\ d e. NN ) -> K = 0 )
32 31 fveq2d 
 |-  ( ( ( ( ph /\ K = 0 ) /\ a e. NN ) /\ d e. NN ) -> ( AP ` K ) = ( AP ` 0 ) )
33 32 oveqd 
 |-  ( ( ( ( ph /\ K = 0 ) /\ a e. NN ) /\ d e. NN ) -> ( a ( AP ` K ) d ) = ( a ( AP ` 0 ) d ) )
34 vdwap0 
 |-  ( ( a e. NN /\ d e. NN ) -> ( a ( AP ` 0 ) d ) = (/) )
35 34 adantll 
 |-  ( ( ( ( ph /\ K = 0 ) /\ a e. NN ) /\ d e. NN ) -> ( a ( AP ` 0 ) d ) = (/) )
36 33 35 eqtrd 
 |-  ( ( ( ( ph /\ K = 0 ) /\ a e. NN ) /\ d e. NN ) -> ( a ( AP ` K ) d ) = (/) )
37 0ss 
 |-  (/) C_ ( `' F " { c } )
38 36 37 eqsstrdi 
 |-  ( ( ( ( ph /\ K = 0 ) /\ a e. NN ) /\ d e. NN ) -> ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
39 38 ralrimiva 
 |-  ( ( ( ph /\ K = 0 ) /\ a e. NN ) -> A. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
40 r19.2z 
 |-  ( ( NN =/= (/) /\ A. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) -> E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
41 30 39 40 sylancr 
 |-  ( ( ( ph /\ K = 0 ) /\ a e. NN ) -> E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
42 41 ralrimiva 
 |-  ( ( ph /\ K = 0 ) -> A. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
43 r19.2z 
 |-  ( ( NN =/= (/) /\ A. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) -> E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
44 30 42 43 sylancr 
 |-  ( ( ph /\ K = 0 ) -> E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
45 44 ralrimivw 
 |-  ( ( ph /\ K = 0 ) -> A. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
46 r19.2z 
 |-  ( ( R =/= (/) /\ A. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) -> E. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
47 28 45 46 syl2an2r 
 |-  ( ( ph /\ K = 0 ) -> E. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
48 rexex 
 |-  ( E. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) -> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
49 47 48 syl 
 |-  ( ( ph /\ K = 0 ) -> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
50 49 47 2thd 
 |-  ( ( ph /\ K = 0 ) -> ( E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> E. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
51 elnn0 
 |-  ( K e. NN0 <-> ( K e. NN \/ K = 0 ) )
52 2 51 sylib 
 |-  ( ph -> ( K e. NN \/ K = 0 ) )
53 26 50 52 mpjaodan 
 |-  ( ph -> ( E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> E. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
54 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 ) ) ) )
55 54 3expb 
 |-  ( ( 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 ) ) ) )
56 2 55 sylan 
 |-  ( ( ph /\ ( a e. NN /\ d e. NN ) ) -> ( x e. ( a ( AP ` K ) d ) <-> E. m e. ( 0 ... ( K - 1 ) ) x = ( a + ( m x. d ) ) ) )
57 56 imbi1d 
 |-  ( ( ph /\ ( a e. NN /\ d e. NN ) ) -> ( ( x e. ( a ( AP ` K ) d ) -> x e. ( `' F " { c } ) ) <-> ( E. m e. ( 0 ... ( K - 1 ) ) x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) ) )
58 57 albidv 
 |-  ( ( ph /\ ( a e. NN /\ d e. NN ) ) -> ( A. x ( x e. ( a ( AP ` K ) d ) -> x e. ( `' F " { c } ) ) <-> A. x ( E. m e. ( 0 ... ( K - 1 ) ) x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) ) )
59 df-ss 
 |-  ( ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> A. x ( x e. ( a ( AP ` K ) d ) -> x e. ( `' F " { c } ) ) )
60 ralcom4 
 |-  ( A. m e. ( 0 ... ( K - 1 ) ) A. x ( x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) <-> A. x A. m e. ( 0 ... ( K - 1 ) ) ( x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) )
61 ovex 
 |-  ( a + ( m x. d ) ) e. _V
62 eleq1 
 |-  ( x = ( a + ( m x. d ) ) -> ( x e. ( `' F " { c } ) <-> ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
63 61 62 ceqsalv 
 |-  ( A. x ( x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) <-> ( a + ( m x. d ) ) e. ( `' F " { c } ) )
64 63 ralbii 
 |-  ( A. m e. ( 0 ... ( K - 1 ) ) A. x ( x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) <-> A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
65 r19.23v 
 |-  ( A. m e. ( 0 ... ( K - 1 ) ) ( x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) <-> ( E. m e. ( 0 ... ( K - 1 ) ) x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) )
66 65 albii 
 |-  ( A. x A. m e. ( 0 ... ( K - 1 ) ) ( x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) <-> A. x ( E. m e. ( 0 ... ( K - 1 ) ) x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) )
67 60 64 66 3bitr3i 
 |-  ( A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> A. x ( E. m e. ( 0 ... ( K - 1 ) ) x = ( a + ( m x. d ) ) -> x e. ( `' F " { c } ) ) )
68 58 59 67 3bitr4g 
 |-  ( ( ph /\ ( a e. NN /\ d e. NN ) ) -> ( ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
69 68 2rexbidva 
 |-  ( ph -> ( E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
70 69 rexbidv 
 |-  ( ph -> ( E. c e. R E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) <-> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
71 5 53 70 3bitrd 
 |-  ( ph -> ( K MonoAP F <-> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )