Definition df-qpOLD 31554

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.) Obsolete version of df-qp 31553 as of 10-Oct-2021. (New usage is discouraged.)

Assertion

Ref

Expression

df-qpOLD

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

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

Detailed syntax breakdown of Definition df-qpOLD

Step	Hyp	Ref	Expression
1		cqpOLD 31544	. 2 class QpOLD
2		vp	. . 3 setvar 𝑝
3		cprime 15385	. . 3 class ℙ
4		vb	. . . 4 setvar 𝑏
5		vh	. . . . . . . . . 10 setvar ℎ
6	5	cv 1482	. . . . . . . . 9 class ℎ
7	6	ccnv 5113	. . . . . . . 8 class ◡ℎ
8		cz 11377	. . . . . . . . 9 class ℤ
9		cc0 9936	. . . . . . . . . 10 class 0
10	9	csn 4177	. . . . . . . . 9 class {0}
11	8, 10	cdif 3571	. . . . . . . 8 class (ℤ ∖ {0})
12	7, 11	cima 5117	. . . . . . 7 class (◡ℎ “ (ℤ ∖ {0}))
13		vx	. . . . . . . 8 setvar 𝑥
14	13	cv 1482	. . . . . . 7 class 𝑥
15	12, 14	wss 3574	. . . . . 6 wff (◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥
16		cuz 11687	. . . . . . 7 class ℤ≥
17	16	crn 5115	. . . . . 6 class ran ℤ≥
18	15, 13, 17	wrex 2913	. . . . 5 wff ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥
19	2	cv 1482	. . . . . . . 8 class 𝑝
20		c1 9937	. . . . . . . 8 class 1
21		cmin 10266	. . . . . . . 8 class −
22	19, 20, 21	co 6650	. . . . . . 7 class (𝑝 − 1)
23		cfz 12326	. . . . . . 7 class ...
24	9, 22, 23	co 6650	. . . . . 6 class (0...(𝑝 − 1))
25		cmap 7857	. . . . . 6 class ↑𝑚
26	8, 24, 25	co 6650	. . . . 5 class (ℤ ↑𝑚 (0...(𝑝 − 1)))
27	18, 5, 26	crab 2916	. . . 4 class {ℎ ∈ (ℤ ↑𝑚 (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥}
28		cnx 15854	. . . . . . . . 9 class ndx
29		cbs 15857	. . . . . . . . 9 class Base
30	28, 29	cfv 5888	. . . . . . . 8 class (Base‘ndx)
31	4	cv 1482	. . . . . . . 8 class 𝑏
32	30, 31	cop 4183	. . . . . . 7 class ⟨(Base‘ndx), 𝑏⟩
33		cplusg 15941	. . . . . . . . 9 class +g
34	28, 33	cfv 5888	. . . . . . . 8 class (+g‘ndx)
35		vf	. . . . . . . . 9 setvar 𝑓
36		vg	. . . . . . . . 9 setvar 𝑔
37	35	cv 1482	. . . . . . . . . . 11 class 𝑓
38	36	cv 1482	. . . . . . . . . . 11 class 𝑔
39		caddc 9939	. . . . . . . . . . . 12 class +
40	39	cof 6895	. . . . . . . . . . 11 class ∘𝑓 +
41	37, 38, 40	co 6650	. . . . . . . . . 10 class (𝑓 ∘𝑓 + 𝑔)
42		crqp 31542	. . . . . . . . . . 11 class /Qp
43	19, 42	cfv 5888	. . . . . . . . . 10 class (/Qp‘𝑝)
44	41, 43	cfv 5888	. . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔))
45	35, 36, 31, 31, 44	cmpt2 6652	. . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔)))
46	34, 45	cop 4183	. . . . . . 7 class ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔)))⟩
47		cmulr 15942	. . . . . . . . 9 class .r
48	28, 47	cfv 5888	. . . . . . . 8 class (.r‘ndx)
49		vn	. . . . . . . . . . 11 setvar 𝑛
50		vk	. . . . . . . . . . . . . . 15 setvar 𝑘
51	50	cv 1482	. . . . . . . . . . . . . 14 class 𝑘
52	51, 37	cfv 5888	. . . . . . . . . . . . 13 class (𝑓‘𝑘)
53	49	cv 1482	. . . . . . . . . . . . . . 15 class 𝑛
54	53, 51, 21	co 6650	. . . . . . . . . . . . . 14 class (𝑛 − 𝑘)
55	54, 38	cfv 5888	. . . . . . . . . . . . 13 class (𝑔‘(𝑛 − 𝑘))
56		cmul 9941	. . . . . . . . . . . . 13 class ·
57	52, 55, 56	co 6650	. . . . . . . . . . . 12 class ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))
58	8, 57, 50	csu 14416	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))
59	49, 8, 58	cmpt 4729	. . . . . . . . . 10 class (𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))
60	59, 43	cfv 5888	. . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))))
61	35, 36, 31, 31, 60	cmpt2 6652	. . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))
62	48, 61	cop 4183	. . . . . . 7 class ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩
63	32, 46, 62	ctp 4181	. . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩}
64		cple 15948	. . . . . . . . 9 class le
65	28, 64	cfv 5888	. . . . . . . 8 class (le‘ndx)
66	37, 38	cpr 4179	. . . . . . . . . . 11 class {𝑓, 𝑔}
67	66, 31	wss 3574	. . . . . . . . . 10 wff {𝑓, 𝑔} ⊆ 𝑏
68	51	cneg 10267	. . . . . . . . . . . . . 14 class -𝑘
69	68, 37	cfv 5888	. . . . . . . . . . . . 13 class (𝑓‘-𝑘)
70	19, 20, 39	co 6650	. . . . . . . . . . . . . 14 class (𝑝 + 1)
71		cexp 12860	. . . . . . . . . . . . . 14 class ↑
72	70, 68, 71	co 6650	. . . . . . . . . . . . 13 class ((𝑝 + 1)↑-𝑘)
73	69, 72, 56	co 6650	. . . . . . . . . . . 12 class ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
74	8, 73, 50	csu 14416	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
75	68, 38	cfv 5888	. . . . . . . . . . . . 13 class (𝑔‘-𝑘)
76	75, 72, 56	co 6650	. . . . . . . . . . . 12 class ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
77	8, 76, 50	csu 14416	. . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
78		clt 10074	. . . . . . . . . . 11 class <
79	74, 77, 78	wbr 4653	. . . . . . . . . 10 wff Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
80	67, 79	wa 384	. . . . . . . . 9 wff ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))
81	80, 35, 36	copab 4712	. . . . . . . 8 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}
82	65, 81	cop 4183	. . . . . . 7 class ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩
83	82	csn 4177	. . . . . 6 class {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}
84	63, 83	cun 3572	. . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩})
85	8, 10	cxp 5112	. . . . . . . 8 class (ℤ × {0})
86	37, 85	wceq 1483	. . . . . . 7 wff 𝑓 = (ℤ × {0})
87	37	ccnv 5113	. . . . . . . . . . 11 class ◡𝑓
88	87, 11	cima 5117	. . . . . . . . . 10 class (◡𝑓 “ (ℤ ∖ {0}))
89		cr 9935	. . . . . . . . . 10 class ℝ
90	78	ccnv 5113	. . . . . . . . . 10 class ◡ <
91	88, 89, 90	csup 8346	. . . . . . . . 9 class sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < )
92	91	cneg 10267	. . . . . . . 8 class -sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < )
93	19, 92, 71	co 6650	. . . . . . 7 class (𝑝↑-sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < ))
94	86, 9, 93	cif 4086	. . . . . 6 class if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < )))
95	35, 31, 94	cmpt 4729	. . . . 5 class (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < ))))
96		ctng 22383	. . . . 5 class toNrmGrp
97	84, 95, 96	co 6650	. . . 4 class (({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < )))))
98	4, 27, 97	csb 3533	. . 3 class ⦋{ℎ ∈ (ℤ ↑𝑚 (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < )))))
99	2, 3, 98	cmpt 4729	. 2 class (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑𝑚 (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < ))))))
100	1, 99	wceq 1483	1 wff QpOLD = (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑𝑚 (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((◡𝑓 “ (ℤ ∖ {0})), ℝ, ◡ < ))))))

This definition is referenced by: (None)