Definition df-qp

Description: Define the p -adic completion of the rational numbers, as a normed field structure with a total order (that is not compatible with the operations). (Contributed by Mario Carneiro, 2-Dec-2014) (Revised by AV, 10-Oct-2021)

	Ref	Expression
Assertion	df-qp	$$⊢{\mathbb{Q}}_p=\left(p\in \mathbb{P}⟼⦋\left\{h\in \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{h}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/b⦌\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}⟩\right\}\right)\mathrm{toNrmGrp}\left(f\in b⟼if\left(f=\mathbb{Z}\times \left\{0\right\},0,p^{-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)}\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqp	$$class{\mathbb{Q}}_p$$
1		vp	$$setvarp$$
2		cprime	$$class\mathbb{P}$$
3		vh	$$setvarh$$
4		cz	$$class\mathbb{Z}$$
5		cmap	$$class{\uparrow }_{𝑚}$$
6		cc0	$$class0$$
7		cfz	$$class\dots$$
8	1	cv	$$setvarp$$
9		cmin	$$class-$$
10		c1	$$class1$$
11	8 10 9	co	$$class\left(p-1\right)$$
12	6 11 7	co	$$class\left(0\dots p-1\right)$$
13	4 12 5	co	$$class\left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)$$
14		vx	$$setvarx$$
15		cuz	$$class{\mathbb{Z}}_{\ge }$$
16	15	crn	$$class\mathrm{ran}{\mathbb{Z}}_{\ge }$$
17	3	cv	$$setvarh$$
18	17	ccnv	$$class{h}^{-1}$$
19	6	csn	$$class\left\{0\right\}$$
20	4 19	cdif	$$class\left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
21	18 20	cima	$$class{h}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]$$
22	14	cv	$$setvarx$$
23	21 22	wss	$$wff{h}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x$$
24	23 14 16	wrex	$$wff\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{h}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x$$
25	24 3 13	crab	$$class\left\{h\in \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{h}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}$$
26		vb	$$setvarb$$
27		cbs	$$class\mathrm{Base}$$
28		cnx	$$class\mathrm{ndx}$$
29	28 27	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
30	26	cv	$$setvarb$$
31	29 30	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩$$
32		cplusg	$$class{+}_{𝑔}$$
33	28 32	cfv	$$class{+}_{\mathrm{ndx}}$$
34		vf	$$setvarf$$
35		vg	$$setvarg$$
36		crqp	$$class{/}_{{\mathbb{Q}}_p}$$
37	8 36	cfv	$$class{/}_{{\mathbb{Q}}_p}\left(p\right)$$
38	34	cv	$$setvarf$$
39		caddc	$$class+$$
40	39	cof	$$class{\circ }_f+$$
41	35	cv	$$setvarg$$
42	38 41 40	co	$$class\left(f{+}_{f}g\right)$$
43	42 37	cfv	$$class{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)$$
44	34 35 30 30 43	cmpo	$$class\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)$$
45	33 44	cop	$$class⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)⟩$$
46		cmulr	$$class{\cdot }_{𝑟}$$
47	28 46	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
48		vn	$$setvarn$$
49		vk	$$setvark$$
50	49	cv	$$setvark$$
51	50 38	cfv	$$classf\left(k\right)$$
52		cmul	$$class\times$$
53	48	cv	$$setvarn$$
54	53 50 9	co	$$class\left(n-k\right)$$
55	54 41	cfv	$$classg\left(n-k\right)$$
56	51 55 52	co	$$classf\left(k\right)g\left(n-k\right)$$
57	4 56 49	csu	$$class\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)$$
58	48 4 57	cmpt	$$class\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)$$
59	58 37	cfv	$$class{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)$$
60	34 35 30 30 59	cmpo	$$class\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)$$
61	47 60	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)⟩$$
62	31 45 61	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)⟩\right\}$$
63		cple	$$class\mathrm{le}$$
64	28 63	cfv	$$class{\le }_{\mathrm{ndx}}$$
65	38 41	cpr	$$class\left\{f,g\right\}$$
66	65 30	wss	$$wff\left\{f,g\right\}\subseteq b$$
67	50	cneg	$$class\left(-k\right)$$
68	67 38	cfv	$$classf\left(-k\right)$$
69	8 10 39	co	$$class\left(p+1\right)$$
70		cexp	$$class^$$
71	69 67 70	co	$$class{\left(p+1\right)}^{-k}$$
72	68 71 52	co	$$classf\left(-k\right){\left(p+1\right)}^{-k}$$
73	4 72 49	csu	$$class\sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}$$
74		clt	$$class<$$
75	67 41	cfv	$$classg\left(-k\right)$$
76	75 71 52	co	$$classg\left(-k\right){\left(p+1\right)}^{-k}$$
77	4 76 49	csu	$$class\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}$$
78	73 77 74	wbr	$$wff\sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}$$
79	66 78	wa	$$wff\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)$$
80	79 34 35	copab	$$class\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}$$
81	64 80	cop	$$class⟨{\le }_{\mathrm{ndx}},\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}⟩$$
82	81	csn	$$class\left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}⟩\right\}$$
83	62 82	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}⟩\right\}\right)$$
84		ctng	$$class\mathrm{toNrmGrp}$$
85	4 19	cxp	$$class\left(\mathbb{Z}\times \left\{0\right\}\right)$$
86	38 85	wceq	$$wfff=\mathbb{Z}\times \left\{0\right\}$$
87	38	ccnv	$$class{f}^{-1}$$
88	87 20	cima	$$class{f}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]$$
89		cr	$$classℝ$$
90	88 89 74	cinf	$$classinf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)$$
91	90	cneg	$$class\left(-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)\right)$$
92	8 91 70	co	$$class{p}^{-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)}$$
93	86 6 92	cif	$$classif\left(f=\mathbb{Z}\times \left\{0\right\},0,p^{-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)}\right)$$
94	34 30 93	cmpt	$$class\left(f\in b⟼if\left(f=\mathbb{Z}\times \left\{0\right\},0,p^{-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)}\right)\right)$$
95	83 94 84	co	$$class\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}⟩\right\}\right)\mathrm{toNrmGrp}\left(f\in b⟼if\left(f=\mathbb{Z}\times \left\{0\right\},0,p^{-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)}\right)\right)\right)$$
96	26 25 95	csb	$$class⦋\left\{h\in \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{h}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/b⦌\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}⟩\right\}\right)\mathrm{toNrmGrp}\left(f\in b⟼if\left(f=\mathbb{Z}\times \left\{0\right\},0,p^{-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)}\right)\right)\right)$$
97	1 2 96	cmpt	$$class\left(p\in \mathbb{P}⟼⦋\left\{h\in \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{h}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/b⦌\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}⟩\right\}\right)\mathrm{toNrmGrp}\left(f\in b⟼if\left(f=\mathbb{Z}\times \left\{0\right\},0,p^{-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)}\right)\right)\right)\right)$$
98	0 97	wceq	$$wff{\mathbb{Q}}_p=\left(p\in \mathbb{P}⟼⦋\left\{h\in \left({\mathbb{Z}}^{\left(0\dots p-1\right)}\right)|\exists x\in \mathrm{ran}{\mathbb{Z}}_{\ge }{h}^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right]\subseteq x\right\}/b⦌\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(f{+}_{f}g\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼{/}_{{\mathbb{Q}}_p}\left(p\right)\left(\left(n\in \mathbb{Z}⟼\sum _{k\in \mathbb{Z}}f\left(k\right)g\left(n-k\right)\right)\right)\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq b\wedge \sum _{k\in \mathbb{Z}}f\left(-k\right){\left(p+1\right)}^{-k}<\sum _{k\in \mathbb{Z}}g\left(-k\right){\left(p+1\right)}^{-k}\right)\right\}⟩\right\}\right)\mathrm{toNrmGrp}\left(f\in b⟼if\left(f=\mathbb{Z}\times \left\{0\right\},0,p^{-inf\left(f^{-1}\left[\mathbb{Z}\setminus \left\{0\right\}\right],ℝ,<\right)}\right)\right)\right)\right)$$