Definition df-qp 36395

Description: Define the 𝑝-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.)

Assertion

Ref

Expression

df-qp

⊢ Qp = (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))))))

Distinct variable group:   𝑓,𝑏,𝑔,ℎ,𝑘,𝑛,𝑝,𝑥

Detailed syntax breakdown of Definition df-qp

Step	Hyp	Ref	Expression
1		cqp 36386	. 2 class Qp
2		vp	. . 3 setvar 𝑝
3		cprime 16826	. . 3 class ℙ
4		vb	. . . 4 setvar 𝑏
5		vh	. . . . . . . . . 10 setvar ℎ
6	5	cv 1569	. . . . . . . . 9 class ℎ
7	6	ccnv 5650	. . . . . . . 8 class ◡ℎ
8		cz 12674	. . . . . . . . 9 class ℤ
9		cc0 11181	. . . . . . . . . 10 class 0
10	9	csn 4584	. . . . . . . . 9 class {0}
11	8, 10	cdif 3896	. . . . . . . 8 class (ℤ ∖ {0})
12	7, 11	cima 5654	. . . . . . 7 class (◡ℎ “ (ℤ ∖ {0}))
13		vx	. . . . . . . 8 setvar 𝑥
14	13	cv 1569	. . . . . . 7 class 𝑥
15	12, 14	wss 3899	. . . . . 6 wff (◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥
16		cuz 12946	. . . . . . 7 class ℤ≥
17	16	crn 5652	. . . . . 6 class ran ℤ≥
18	15, 13, 17	wrex 3087	. . . . 5 wff ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥
19	2	cv 1569	. . . . . . . 8 class 𝑝
20		c1 11182	. . . . . . . 8 class 1
21		cmin 11522	. . . . . . . 8 class −
22	19, 20, 21	co 7412	. . . . . . 7 class (𝑝 − 1)
23		cfz 13620	. . . . . . 7 class ...
24	9, 22, 23	co 7412	. . . . . 6 class (0...(𝑝 − 1))
25		cmap 8831	. . . . . 6 class ↑m
26	8, 24, 25	co 7412	. . . . 5 class (ℤ ↑m (0...(𝑝 − 1)))
27	18, 5, 26	crab 3413	. . . 4 class {ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥}
28		cnx 17351	. . . . . . . . 9 class ndx
29		cbs 17367	. . . . . . . . 9 class Base
30	28, 29	cfv 6531	. . . . . . . 8 class (Base‘ndx)
31	4	cv 1569	. . . . . . . 8 class 𝑏
32	30, 31	cop 4590	. . . . . . 7 class ⟨(Base‘ndx), 𝑏⟩
33		cplusg 17408	. . . . . . . . 9 class +g
34	28, 33	cfv 6531	. . . . . . . 8 class (+g‘ndx)
35		vf	. . . . . . . . 9 setvar 𝑓
36		vg	. . . . . . . . 9 setvar 𝑔
37	35	cv 1569	. . . . . . . . . . 11 class 𝑓
38	36	cv 1569	. . . . . . . . . . 11 class 𝑔
39		caddc 11184	. . . . . . . . . . . 12 class +
40	39	cof 7680	. . . . . . . . . . 11 class ∘f +
41	37, 38, 40	co 7412	. . . . . . . . . 10 class (𝑓 ∘f + 𝑔)
42		crqp 36385	. . . . . . . . . . 11 class /Qp
43	19, 42	cfv 6531	. . . . . . . . . 10 class (/Qp‘𝑝)
44	41, 43	cfv 6531	. . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔))
45	35, 36, 31, 31, 44	cmpo 7414	. . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))
46	34, 45	cop 4590	. . . . . . 7 class ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩
47		cmulr 17409	. . . . . . . . 9 class .r
48	28, 47	cfv 6531	. . . . . . . 8 class (.r‘ndx)
49		vn	. . . . . . . . . . 11 setvar 𝑛
50		vk	. . . . . . . . . . . . . . 15 setvar 𝑘
51	50	cv 1569	. . . . . . . . . . . . . 14 class 𝑘
52	51, 37	cfv 6531	. . . . . . . . . . . . 13 class (𝑓‘𝑘)
53	49	cv 1569	. . . . . . . . . . . . . . 15 class 𝑛
54	53, 51, 21	co 7412	. . . . . . . . . . . . . 14 class (𝑛 − 𝑘)
55	54, 38	cfv 6531	. . . . . . . . . . . . 13 class (𝑔‘(𝑛 − 𝑘))
56		cmul 11186	. . . . . . . . . . . . 13 class ·
57	52, 55, 56	co 7412	. . . . . . . . . . . 12 class ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))
58	8, 57, 50	csu 15833	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))
59	49, 8, 58	cmpt 5186	. . . . . . . . . 10 class (𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))
60	59, 43	cfv 6531	. . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))))
61	35, 36, 31, 31, 60	cmpo 7414	. . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))
62	48, 61	cop 4590	. . . . . . 7 class ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩
63	32, 46, 62	ctp 4588	. . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩}
64		cple 17415	. . . . . . . . 9 class le
65	28, 64	cfv 6531	. . . . . . . 8 class (le‘ndx)
66	37, 38	cpr 4586	. . . . . . . . . . 11 class {𝑓, 𝑔}
67	66, 31	wss 3899	. . . . . . . . . 10 wff {𝑓, 𝑔} ⊆ 𝑏
68	51	cneg 11523	. . . . . . . . . . . . . 14 class -𝑘
69	68, 37	cfv 6531	. . . . . . . . . . . . 13 class (𝑓‘-𝑘)
70	19, 20, 39	co 7412	. . . . . . . . . . . . . 14 class (𝑝 + 1)
71		cexp 14184	. . . . . . . . . . . . . 14 class ↑
72	70, 68, 71	co 7412	. . . . . . . . . . . . 13 class ((𝑝 + 1)↑-𝑘)
73	69, 72, 56	co 7412	. . . . . . . . . . . 12 class ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
74	8, 73, 50	csu 15833	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
75	68, 38	cfv 6531	. . . . . . . . . . . . 13 class (𝑔‘-𝑘)
76	75, 72, 56	co 7412	. . . . . . . . . . . 12 class ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
77	8, 76, 50	csu 15833	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
78		clt 11324	. . . . . . . . . . 11 class <
79	74, 77, 78	wbr 5103	. . . . . . . . . 10 wff Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
80	67, 79	wa 401	. . . . . . . . 9 wff ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))
81	80, 35, 36	copab 5167	. . . . . . . 8 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}
82	65, 81	cop 4590	. . . . . . 7 class ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩
83	82	csn 4584	. . . . . 6 class {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}
84	63, 83	cun 3897	. . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩})
85	8, 10	cxp 5649	. . . . . . . 8 class (ℤ × {0})
86	37, 85	wceq 1570	. . . . . . 7 wff 𝑓 = (ℤ × {0})
87	37	ccnv 5650	. . . . . . . . . . 11 class ◡𝑓
88	87, 11	cima 5654	. . . . . . . . . 10 class (◡𝑓 “ (ℤ ∖ {0}))
89		cr 11180	. . . . . . . . . 10 class ℝ
90	88, 89, 78	cinf 9417	. . . . . . . . 9 class inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )
91	90	cneg 11523	. . . . . . . 8 class -inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )
92	19, 91, 71	co 7412	. . . . . . 7 class (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))
93	86, 9, 92	cif 4482	. . . . . 6 class if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )))
94	35, 31, 93	cmpt 5186	. . . . 5 class (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))))
95		ctng 24877	. . . . 5 class toNrmGrp
96	84, 94, 95	co 7412	. . . 4 class (({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )))))
97	4, 27, 96	csb 3847	. . 3 class ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )))))
98	2, 3, 97	cmpt 5186	. 2 class (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))))))
99	1, 98	wceq 1570	1 wff Qp = (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))))))

This definition is used by: (None)