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	$$⊢{/}_{{\mathbb{Q}}_p}=\left(p\in \mathbb{P}⟼{~}_{{\mathbb{Q}}_p}\cap ⦋\left\{f\in \left({\mathbb{Z}}^{\mathbb{Z}}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/y⦌\left(y\times \left(y\cap \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crqp	$$class{/}_{{\mathbb{Q}}_p}$$
1		vp	$$setvarp$$
2		cprime	$$class\mathbb{P}$$
3		ceqp	$$class{~}_{{\mathbb{Q}}_p}$$
4		vf	$$setvarf$$
5		cz	$$class\mathbb{Z}$$
6		cmap	$$class{\uparrow }_{𝑚}$$
7	5 5 6	co	$$class\left({\mathbb{Z}}^{\mathbb{Z}}\right)$$
8		vx	$$setvarx$$
9		cuz	$$class{\mathbb{Z}}_{\ge }$$
10	9	crn	$$class\mathrm{ran}{\mathbb{Z}}_{\ge }$$
11	4	cv	$$setvarf$$
12	11	ccnv	$$class{f}^{-1}$$
13		cc0	$$class0$$
14	13	csn	$$class\left\{0\right\}$$
15	5 14	cdif	$$class\left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
16	12 15	cima	$$class{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]$$
17	8	cv	$$setvarx$$
18	16 17	wss	$$wff{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x$$
19	18 8 10	wrex	$$wff\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x$$
20	19 4 7	crab	$$class\left\{f\in \left({\mathbb{Z}}^{\mathbb{Z}}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}$$
21		vy	$$setvary$$
22	21	cv	$$setvary$$
23		cfz	$$class\dots$$
24	1	cv	$$setvarp$$
25		cmin	$$class-$$
26		c1	$$class1$$
27	24 26 25	co	$$class\left(p-1\right)$$
28	13 27 23	co	$$class\left(0\dots p-1\right)$$
29	5 28 6	co	$$class\left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)$$
30	22 29	cin	$$class\left(y\cap \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)\right)$$
31	22 30	cxp	$$class\left(y\times \left(y\cap \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)\right)\right)$$
32	21 20 31	csb	$$class⦋\left\{f\in \left({\mathbb{Z}}^{\mathbb{Z}}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/y⦌\left(y\times \left(y\cap \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)\right)\right)$$
33	3 32	cin	$$class\left({~}_{{\mathbb{Q}}_p}\cap ⦋\left\{f\in \left({\mathbb{Z}}^{\mathbb{Z}}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/y⦌\left(y\times \left(y\cap \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)\right)\right)\right)$$
34	1 2 33	cmpt	$$class\left(p\in \mathbb{P}⟼{~}_{{\mathbb{Q}}_p}\cap ⦋\left\{f\in \left({\mathbb{Z}}^{\mathbb{Z}}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/y⦌\left(y\times \left(y\cap \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)\right)\right)\right)$$
35	0 34	wceq	$$wff{/}_{{\mathbb{Q}}_p}=\left(p\in \mathbb{P}⟼{~}_{{\mathbb{Q}}_p}\cap ⦋\left\{f\in \left({\mathbb{Z}}^{\mathbb{Z}}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/y⦌\left(y\times \left(y\cap \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)\right)\right)\right)$$