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 = ( 𝑝 ∈ ℙ ↦ ( ~Qp ∩ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crqp	⊢ /Qp
1		vp	⊢ 𝑝
2		cprime	⊢ ℙ
3		ceqp	⊢ ~Qp
4		vf	⊢ 𝑓
5		cz	⊢ ℤ
6		cmap	⊢ ↑m
7	5 5 6	co	⊢ ( ℤ ↑m ℤ )
8		vx	⊢ 𝑥
9		cuz	⊢ ℤ≥
10	9	crn	⊢ ran ℤ≥
11	4	cv	⊢ 𝑓
12	11	ccnv	⊢ ◡ 𝑓
13		cc0	⊢ 0
14	13	csn	⊢ { 0 }
15	5 14	cdif	⊢ ( ℤ ∖ { 0 } )
16	12 15	cima	⊢ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) )
17	8	cv	⊢ 𝑥
18	16 17	wss	⊢ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥
19	18 8 10	wrex	⊢ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥
20	19 4 7	crab	⊢ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 }
21		vy	⊢ 𝑦
22	21	cv	⊢ 𝑦
23		cfz	⊢ ...
24	1	cv	⊢ 𝑝
25		cmin	⊢ −
26		c1	⊢ 1
27	24 26 25	co	⊢ ( 𝑝 − 1 )
28	13 27 23	co	⊢ ( 0 ... ( 𝑝 − 1 ) )
29	5 28 6	co	⊢ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) )
30	22 29	cin	⊢ ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) )
31	22 30	cxp	⊢ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) )
32	21 20 31	csb	⊢ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) )
33	3 32	cin	⊢ ( ~Qp ∩ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) )
34	1 2 33	cmpt	⊢ ( 𝑝 ∈ ℙ ↦ ( ~Qp ∩ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) ) )
35	0 34	wceq	⊢ /Qp = ( 𝑝 ∈ ℙ ↦ ( ~Qp ∩ ⦋ { 𝑓 ∈ ( ℤ ↑m ℤ ) ∣ ∃ 𝑥 ∈ ran ℤ≥ ( ◡ 𝑓 “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑦 ⦌ ( 𝑦 × ( 𝑦 ∩ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ) ) ) )