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 /p = p ~p f | x ran f -1 0 x / y y × y 0 p 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 crqp class /p
1 vp setvar p
2 cprime class
3 ceqp class ~p
4 vf setvar f
5 cz class
6 cmap class 𝑚
7 5 5 6 co class
8 vx setvar x
9 cuz class
10 9 crn class ran
11 4 cv setvar f
12 11 ccnv class f -1
13 cc0 class 0
14 13 csn class 0
15 5 14 cdif class 0
16 12 15 cima class f -1 0
17 8 cv setvar x
18 16 17 wss wff f -1 0 x
19 18 8 10 wrex wff x ran f -1 0 x
20 19 4 7 crab class f | x ran f -1 0 x
21 vy setvar y
22 21 cv setvar y
23 cfz class
24 1 cv setvar p
25 cmin class
26 c1 class 1
27 24 26 25 co class p 1
28 13 27 23 co class 0 p 1
29 5 28 6 co class 0 p 1
30 22 29 cin class y 0 p 1
31 22 30 cxp class y × y 0 p 1
32 21 20 31 csb class f | x ran f -1 0 x / y y × y 0 p 1
33 3 32 cin class ~p f | x ran f -1 0 x / y y × y 0 p 1
34 1 2 33 cmpt class p ~p f | x ran f -1 0 x / y y × y 0 p 1
35 0 34 wceq wff /p = p ~p f | x ran f -1 0 x / y y × y 0 p 1