Metamath Proof Explorer

Definition df-rqp

Description: There is a unique element of ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ~Qp -equivalent to any element of ( ZZ ^m ZZ ) , if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-rqp 
|- /Qp = ( p e. Prime |-> ( ~Qp i^i [_ { f e. ( ZZ ^m ZZ ) | E. x e. ran ZZ>= ( `' f " ( ZZ \ { 0 } ) ) C_ x } / y ]_ ( y X. ( y i^i ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crqp 
 |-  /Qp
1 vp 
 |-  p
2 cprime 
 |-  Prime
3 ceqp 
 |-  ~Qp
4 vf 
 |-  f
5 cz 
 |-  ZZ
6 cmap 
 |-  ^m
7 5 5 6 co 
 |-  ( ZZ ^m ZZ )
8 vx 
 |-  x
9 cuz 
 |-  ZZ>=
10 9 crn 
 |-  ran ZZ>=
11 4 cv 
 |-  f
12 11 ccnv 
 |-  `' f
13 cc0 
 |-  0
14 13 csn 
 |-  { 0 }
15 5 14 cdif 
 |-  ( ZZ \ { 0 } )
16 12 15 cima 
 |-  ( `' f " ( ZZ \ { 0 } ) )
17 8 cv 
 |-  x
18 16 17 wss 
 |-  ( `' f " ( ZZ \ { 0 } ) ) C_ x
19 18 8 10 wrex 
 |-  E. x e. ran ZZ>= ( `' f " ( ZZ \ { 0 } ) ) C_ x
20 19 4 7 crab 
 |-  { f e. ( ZZ ^m ZZ ) | E. x e. ran ZZ>= ( `' f " ( ZZ \ { 0 } ) ) C_ x }
21 vy 
 |-  y
22 21 cv 
 |-  y
23 cfz 
 |-  ...
24 1 cv 
 |-  p
25 cmin 
 |-  -
26 c1 
 |-  1
27 24 26 25 co 
 |-  ( p - 1 )
28 13 27 23 co 
 |-  ( 0 ... ( p - 1 ) )
29 5 28 6 co 
 |-  ( ZZ ^m ( 0 ... ( p - 1 ) ) )
30 22 29 cin 
 |-  ( y i^i ( ZZ ^m ( 0 ... ( p - 1 ) ) ) )
31 22 30 cxp 
 |-  ( y X. ( y i^i ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ) )
32 21 20 31 csb 
 |-  [_ { f e. ( ZZ ^m ZZ ) | E. x e. ran ZZ>= ( `' f " ( ZZ \ { 0 } ) ) C_ x } / y ]_ ( y X. ( y i^i ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ) )
33 3 32 cin 
 |-  ( ~Qp i^i [_ { f e. ( ZZ ^m ZZ ) | E. x e. ran ZZ>= ( `' f " ( ZZ \ { 0 } ) ) C_ x } / y ]_ ( y X. ( y i^i ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ) ) )
34 1 2 33 cmpt 
 |-  ( p e. Prime |-> ( ~Qp i^i [_ { f e. ( ZZ ^m ZZ ) | E. x e. ran ZZ>= ( `' f " ( ZZ \ { 0 } ) ) C_ x } / y ]_ ( y X. ( y i^i ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ) ) ) )
35 0 34 wceq 
 |-  /Qp = ( p e. Prime |-> ( ~Qp i^i [_ { f e. ( ZZ ^m ZZ ) | E. x e. ran ZZ>= ( `' f " ( ZZ \ { 0 } ) ) C_ x } / y ]_ ( y X. ( y i^i ( ZZ ^m ( 0 ... ( p - 1 ) ) ) ) ) ) )