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 = ( 𝑝 ∈ ℙ ↦ ( ~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 ) ) ) ) ) ) )