Definition df-qp 33598

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 33589	. 2 class Qp
2		vp	. . 3 setvar 𝑝
3		cprime 16357	. . 3 class ℙ
4		vb	. . . 4 setvar 𝑏
5		vh	. . . . . . . . . 10 setvar ℎ
6	5	cv 1540	. . . . . . . . 9 class ℎ
7	6	ccnv 5587	. . . . . . . 8 class ◡ℎ
8		cz 12302	. . . . . . . . 9 class ℤ
9		cc0 10855	. . . . . . . . . 10 class 0
10	9	csn 4566	. . . . . . . . 9 class {0}
11	8, 10	cdif 3888	. . . . . . . 8 class (ℤ ∖ {0})
12	7, 11	cima 5591	. . . . . . 7 class (◡ℎ “ (ℤ ∖ {0}))
13		vx	. . . . . . . 8 setvar 𝑥
14	13	cv 1540	. . . . . . 7 class 𝑥
15	12, 14	wss 3891	. . . . . 6 wff (◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥
16		cuz 12564	. . . . . . 7 class ℤ≥
17	16	crn 5589	. . . . . 6 class ran ℤ≥
18	15, 13, 17	wrex 3066	. . . . 5 wff ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥
19	2	cv 1540	. . . . . . . 8 class 𝑝
20		c1 10856	. . . . . . . 8 class 1
21		cmin 11188	. . . . . . . 8 class −
22	19, 20, 21	co 7268	. . . . . . 7 class (𝑝 − 1)
23		cfz 13221	. . . . . . 7 class ...
24	9, 22, 23	co 7268	. . . . . 6 class (0...(𝑝 − 1))
25		cmap 8589	. . . . . 6 class ↑m
26	8, 24, 25	co 7268	. . . . 5 class (ℤ ↑m (0...(𝑝 − 1)))
27	18, 5, 26	crab 3069	. . . 4 class {ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥}
28		cnx 16875	. . . . . . . . 9 class ndx
29		cbs 16893	. . . . . . . . 9 class Base
30	28, 29	cfv 6430	. . . . . . . 8 class (Base‘ndx)
31	4	cv 1540	. . . . . . . 8 class 𝑏
32	30, 31	cop 4572	. . . . . . 7 class ⟨(Base‘ndx), 𝑏⟩
33		cplusg 16943	. . . . . . . . 9 class +g
34	28, 33	cfv 6430	. . . . . . . 8 class (+g‘ndx)
35		vf	. . . . . . . . 9 setvar 𝑓
36		vg	. . . . . . . . 9 setvar 𝑔
37	35	cv 1540	. . . . . . . . . . 11 class 𝑓
38	36	cv 1540	. . . . . . . . . . 11 class 𝑔
39		caddc 10858	. . . . . . . . . . . 12 class +
40	39	cof 7522	. . . . . . . . . . 11 class ∘f +
41	37, 38, 40	co 7268	. . . . . . . . . 10 class (𝑓 ∘f + 𝑔)
42		crqp 33588	. . . . . . . . . . 11 class /Qp
43	19, 42	cfv 6430	. . . . . . . . . 10 class (/Qp‘𝑝)
44	41, 43	cfv 6430	. . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔))
45	35, 36, 31, 31, 44	cmpo 7270	. . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))
46	34, 45	cop 4572	. . . . . . 7 class ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩
47		cmulr 16944	. . . . . . . . 9 class .r
48	28, 47	cfv 6430	. . . . . . . 8 class (.r‘ndx)
49		vn	. . . . . . . . . . 11 setvar 𝑛
50		vk	. . . . . . . . . . . . . . 15 setvar 𝑘
51	50	cv 1540	. . . . . . . . . . . . . 14 class 𝑘
52	51, 37	cfv 6430	. . . . . . . . . . . . 13 class (𝑓‘𝑘)
53	49	cv 1540	. . . . . . . . . . . . . . 15 class 𝑛
54	53, 51, 21	co 7268	. . . . . . . . . . . . . 14 class (𝑛 − 𝑘)
55	54, 38	cfv 6430	. . . . . . . . . . . . 13 class (𝑔‘(𝑛 − 𝑘))
56		cmul 10860	. . . . . . . . . . . . 13 class ·
57	52, 55, 56	co 7268	. . . . . . . . . . . 12 class ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))
58	8, 57, 50	csu 15378	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))
59	49, 8, 58	cmpt 5161	. . . . . . . . . 10 class (𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))
60	59, 43	cfv 6430	. . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))))
61	35, 36, 31, 31, 60	cmpo 7270	. . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))
62	48, 61	cop 4572	. . . . . . 7 class ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩
63	32, 46, 62	ctp 4570	. . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩}
64		cple 16950	. . . . . . . . 9 class le
65	28, 64	cfv 6430	. . . . . . . 8 class (le‘ndx)
66	37, 38	cpr 4568	. . . . . . . . . . 11 class {𝑓, 𝑔}
67	66, 31	wss 3891	. . . . . . . . . 10 wff {𝑓, 𝑔} ⊆ 𝑏
68	51	cneg 11189	. . . . . . . . . . . . . 14 class -𝑘
69	68, 37	cfv 6430	. . . . . . . . . . . . 13 class (𝑓‘-𝑘)
70	19, 20, 39	co 7268	. . . . . . . . . . . . . 14 class (𝑝 + 1)
71		cexp 13763	. . . . . . . . . . . . . 14 class ↑
72	70, 68, 71	co 7268	. . . . . . . . . . . . 13 class ((𝑝 + 1)↑-𝑘)
73	69, 72, 56	co 7268	. . . . . . . . . . . 12 class ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
74	8, 73, 50	csu 15378	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
75	68, 38	cfv 6430	. . . . . . . . . . . . 13 class (𝑔‘-𝑘)
76	75, 72, 56	co 7268	. . . . . . . . . . . 12 class ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
77	8, 76, 50	csu 15378	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
78		clt 10993	. . . . . . . . . . 11 class <
79	74, 77, 78	wbr 5078	. . . . . . . . . 10 wff Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
80	67, 79	wa 395	. . . . . . . . 9 wff ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))
81	80, 35, 36	copab 5140	. . . . . . . 8 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}
82	65, 81	cop 4572	. . . . . . 7 class ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩
83	82	csn 4566	. . . . . 6 class {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}
84	63, 83	cun 3889	. . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩})
85	8, 10	cxp 5586	. . . . . . . 8 class (ℤ × {0})
86	37, 85	wceq 1541	. . . . . . 7 wff 𝑓 = (ℤ × {0})
87	37	ccnv 5587	. . . . . . . . . . 11 class ◡𝑓
88	87, 11	cima 5591	. . . . . . . . . 10 class (◡𝑓 “ (ℤ ∖ {0}))
89		cr 10854	. . . . . . . . . 10 class ℝ
90	88, 89, 78	cinf 9161	. . . . . . . . 9 class inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )
91	90	cneg 11189	. . . . . . . 8 class -inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )
92	19, 91, 71	co 7268	. . . . . . 7 class (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))
93	86, 9, 92	cif 4464	. . . . . 6 class if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )))
94	35, 31, 93	cmpt 5161	. . . . 5 class (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))))
95		ctng 23715	. . . . 5 class toNrmGrp
96	84, 94, 95	co 7268	. . . 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 3836	. . 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 5161	. 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 1541	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 referenced by: (None)