Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-qp Structured version   Visualization version   GIF version

Definition df-qp 33615
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
StepHypRef Expression
1 cqp 33606 . 2 class Qp
2 vp . . 3 setvar 𝑝
3 cprime 16374 . . 3 class
4 vb . . . 4 setvar 𝑏
5 vh . . . . . . . . . 10 setvar
65cv 1541 . . . . . . . . 9 class
76ccnv 5589 . . . . . . . 8 class
8 cz 12319 . . . . . . . . 9 class
9 cc0 10872 . . . . . . . . . 10 class 0
109csn 4567 . . . . . . . . 9 class {0}
118, 10cdif 3889 . . . . . . . 8 class (ℤ ∖ {0})
127, 11cima 5593 . . . . . . 7 class ( “ (ℤ ∖ {0}))
13 vx . . . . . . . 8 setvar 𝑥
1413cv 1541 . . . . . . 7 class 𝑥
1512, 14wss 3892 . . . . . 6 wff ( “ (ℤ ∖ {0})) ⊆ 𝑥
16 cuz 12581 . . . . . . 7 class
1716crn 5591 . . . . . 6 class ran ℤ
1815, 13, 17wrex 3067 . . . . 5 wff 𝑥 ∈ ran ℤ( “ (ℤ ∖ {0})) ⊆ 𝑥
192cv 1541 . . . . . . . 8 class 𝑝
20 c1 10873 . . . . . . . 8 class 1
21 cmin 11205 . . . . . . . 8 class
2219, 20, 21co 7271 . . . . . . 7 class (𝑝 − 1)
23 cfz 13238 . . . . . . 7 class ...
249, 22, 23co 7271 . . . . . 6 class (0...(𝑝 − 1))
25 cmap 8598 . . . . . 6 class m
268, 24, 25co 7271 . . . . 5 class (ℤ ↑m (0...(𝑝 − 1)))
2718, 5, 26crab 3070 . . . 4 class { ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ( “ (ℤ ∖ {0})) ⊆ 𝑥}
28 cnx 16892 . . . . . . . . 9 class ndx
29 cbs 16910 . . . . . . . . 9 class Base
3028, 29cfv 6432 . . . . . . . 8 class (Base‘ndx)
314cv 1541 . . . . . . . 8 class 𝑏
3230, 31cop 4573 . . . . . . 7 class ⟨(Base‘ndx), 𝑏
33 cplusg 16960 . . . . . . . . 9 class +g
3428, 33cfv 6432 . . . . . . . 8 class (+g‘ndx)
35 vf . . . . . . . . 9 setvar 𝑓
36 vg . . . . . . . . 9 setvar 𝑔
3735cv 1541 . . . . . . . . . . 11 class 𝑓
3836cv 1541 . . . . . . . . . . 11 class 𝑔
39 caddc 10875 . . . . . . . . . . . 12 class +
4039cof 7525 . . . . . . . . . . 11 class f +
4137, 38, 40co 7271 . . . . . . . . . 10 class (𝑓f + 𝑔)
42 crqp 33605 . . . . . . . . . . 11 class /Qp
4319, 42cfv 6432 . . . . . . . . . 10 class (/Qp‘𝑝)
4441, 43cfv 6432 . . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑓f + 𝑔))
4535, 36, 31, 31, 44cmpo 7273 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))
4634, 45cop 4573 . . . . . . 7 class ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))⟩
47 cmulr 16961 . . . . . . . . 9 class .r
4828, 47cfv 6432 . . . . . . . 8 class (.r‘ndx)
49 vn . . . . . . . . . . 11 setvar 𝑛
50 vk . . . . . . . . . . . . . . 15 setvar 𝑘
5150cv 1541 . . . . . . . . . . . . . 14 class 𝑘
5251, 37cfv 6432 . . . . . . . . . . . . 13 class (𝑓𝑘)
5349cv 1541 . . . . . . . . . . . . . . 15 class 𝑛
5453, 51, 21co 7271 . . . . . . . . . . . . . 14 class (𝑛𝑘)
5554, 38cfv 6432 . . . . . . . . . . . . 13 class (𝑔‘(𝑛𝑘))
56 cmul 10877 . . . . . . . . . . . . 13 class ·
5752, 55, 56co 7271 . . . . . . . . . . . 12 class ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))
588, 57, 50csu 15395 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))
5949, 8, 58cmpt 5162 . . . . . . . . . 10 class (𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))
6059, 43cfv 6432 . . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))))
6135, 36, 31, 31, 60cmpo 7273 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))
6248, 61cop 4573 . . . . . . 7 class ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩
6332, 46, 62ctp 4571 . . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩}
64 cple 16967 . . . . . . . . 9 class le
6528, 64cfv 6432 . . . . . . . 8 class (le‘ndx)
6637, 38cpr 4569 . . . . . . . . . . 11 class {𝑓, 𝑔}
6766, 31wss 3892 . . . . . . . . . 10 wff {𝑓, 𝑔} ⊆ 𝑏
6851cneg 11206 . . . . . . . . . . . . . 14 class -𝑘
6968, 37cfv 6432 . . . . . . . . . . . . 13 class (𝑓‘-𝑘)
7019, 20, 39co 7271 . . . . . . . . . . . . . 14 class (𝑝 + 1)
71 cexp 13780 . . . . . . . . . . . . . 14 class
7270, 68, 71co 7271 . . . . . . . . . . . . 13 class ((𝑝 + 1)↑-𝑘)
7369, 72, 56co 7271 . . . . . . . . . . . 12 class ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
748, 73, 50csu 15395 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
7568, 38cfv 6432 . . . . . . . . . . . . 13 class (𝑔‘-𝑘)
7675, 72, 56co 7271 . . . . . . . . . . . 12 class ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
778, 76, 50csu 15395 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
78 clt 11010 . . . . . . . . . . 11 class <
7974, 77, 78wbr 5079 . . . . . . . . . 10 wff Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
8067, 79wa 396 . . . . . . . . 9 wff ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))
8180, 35, 36copab 5141 . . . . . . . 8 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}
8265, 81cop 4573 . . . . . . 7 class ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩
8382csn 4567 . . . . . 6 class {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}
8463, 83cun 3890 . . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩})
858, 10cxp 5588 . . . . . . . 8 class (ℤ × {0})
8637, 85wceq 1542 . . . . . . 7 wff 𝑓 = (ℤ × {0})
8737ccnv 5589 . . . . . . . . . . 11 class 𝑓
8887, 11cima 5593 . . . . . . . . . 10 class (𝑓 “ (ℤ ∖ {0}))
89 cr 10871 . . . . . . . . . 10 class
9088, 89, 78cinf 9178 . . . . . . . . 9 class inf((𝑓 “ (ℤ ∖ {0})), ℝ, < )
9190cneg 11206 . . . . . . . 8 class -inf((𝑓 “ (ℤ ∖ {0})), ℝ, < )
9219, 91, 71co 7271 . . . . . . 7 class (𝑝↑-inf((𝑓 “ (ℤ ∖ {0})), ℝ, < ))
9386, 9, 92cif 4465 . . . . . 6 class if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((𝑓 “ (ℤ ∖ {0})), ℝ, < )))
9435, 31, 93cmpt 5162 . . . . 5 class (𝑓𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((𝑓 “ (ℤ ∖ {0})), ℝ, < ))))
95 ctng 23732 . . . . 5 class toNrmGrp
9684, 94, 95co 7271 . . . 4 class (({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((𝑓 “ (ℤ ∖ {0})), ℝ, < )))))
974, 27, 96csb 3837 . . 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})), ℝ, < )))))
982, 3, 97cmpt 5162 . 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})), ℝ, < ))))))
991, 98wceq 1542 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})), ℝ, < ))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator