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 32961
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 32952 . 2 class Qp
2 vp . . 3 setvar 𝑝
3 cprime 16013 . . 3 class
4 vb . . . 4 setvar 𝑏
5 vh . . . . . . . . . 10 setvar
65cv 1537 . . . . . . . . 9 class
76ccnv 5541 . . . . . . . 8 class
8 cz 11978 . . . . . . . . 9 class
9 cc0 10535 . . . . . . . . . 10 class 0
109csn 4550 . . . . . . . . 9 class {0}
118, 10cdif 3916 . . . . . . . 8 class (ℤ ∖ {0})
127, 11cima 5545 . . . . . . 7 class ( “ (ℤ ∖ {0}))
13 vx . . . . . . . 8 setvar 𝑥
1413cv 1537 . . . . . . 7 class 𝑥
1512, 14wss 3919 . . . . . 6 wff ( “ (ℤ ∖ {0})) ⊆ 𝑥
16 cuz 12240 . . . . . . 7 class
1716crn 5543 . . . . . 6 class ran ℤ
1815, 13, 17wrex 3134 . . . . 5 wff 𝑥 ∈ ran ℤ( “ (ℤ ∖ {0})) ⊆ 𝑥
192cv 1537 . . . . . . . 8 class 𝑝
20 c1 10536 . . . . . . . 8 class 1
21 cmin 10868 . . . . . . . 8 class
2219, 20, 21co 7149 . . . . . . 7 class (𝑝 − 1)
23 cfz 12894 . . . . . . 7 class ...
249, 22, 23co 7149 . . . . . 6 class (0...(𝑝 − 1))
25 cmap 8402 . . . . . 6 class m
268, 24, 25co 7149 . . . . 5 class (ℤ ↑m (0...(𝑝 − 1)))
2718, 5, 26crab 3137 . . . 4 class { ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ( “ (ℤ ∖ {0})) ⊆ 𝑥}
28 cnx 16480 . . . . . . . . 9 class ndx
29 cbs 16483 . . . . . . . . 9 class Base
3028, 29cfv 6343 . . . . . . . 8 class (Base‘ndx)
314cv 1537 . . . . . . . 8 class 𝑏
3230, 31cop 4556 . . . . . . 7 class ⟨(Base‘ndx), 𝑏
33 cplusg 16565 . . . . . . . . 9 class +g
3428, 33cfv 6343 . . . . . . . 8 class (+g‘ndx)
35 vf . . . . . . . . 9 setvar 𝑓
36 vg . . . . . . . . 9 setvar 𝑔
3735cv 1537 . . . . . . . . . . 11 class 𝑓
3836cv 1537 . . . . . . . . . . 11 class 𝑔
39 caddc 10538 . . . . . . . . . . . 12 class +
4039cof 7401 . . . . . . . . . . 11 class f +
4137, 38, 40co 7149 . . . . . . . . . 10 class (𝑓f + 𝑔)
42 crqp 32951 . . . . . . . . . . 11 class /Qp
4319, 42cfv 6343 . . . . . . . . . 10 class (/Qp‘𝑝)
4441, 43cfv 6343 . . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑓f + 𝑔))
4535, 36, 31, 31, 44cmpo 7151 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))
4634, 45cop 4556 . . . . . . 7 class ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))⟩
47 cmulr 16566 . . . . . . . . 9 class .r
4828, 47cfv 6343 . . . . . . . 8 class (.r‘ndx)
49 vn . . . . . . . . . . 11 setvar 𝑛
50 vk . . . . . . . . . . . . . . 15 setvar 𝑘
5150cv 1537 . . . . . . . . . . . . . 14 class 𝑘
5251, 37cfv 6343 . . . . . . . . . . . . 13 class (𝑓𝑘)
5349cv 1537 . . . . . . . . . . . . . . 15 class 𝑛
5453, 51, 21co 7149 . . . . . . . . . . . . . 14 class (𝑛𝑘)
5554, 38cfv 6343 . . . . . . . . . . . . 13 class (𝑔‘(𝑛𝑘))
56 cmul 10540 . . . . . . . . . . . . 13 class ·
5752, 55, 56co 7149 . . . . . . . . . . . 12 class ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))
588, 57, 50csu 15042 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))
5949, 8, 58cmpt 5132 . . . . . . . . . 10 class (𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))
6059, 43cfv 6343 . . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))))
6135, 36, 31, 31, 60cmpo 7151 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))
6248, 61cop 4556 . . . . . . 7 class ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩
6332, 46, 62ctp 4554 . . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩}
64 cple 16572 . . . . . . . . 9 class le
6528, 64cfv 6343 . . . . . . . 8 class (le‘ndx)
6637, 38cpr 4552 . . . . . . . . . . 11 class {𝑓, 𝑔}
6766, 31wss 3919 . . . . . . . . . 10 wff {𝑓, 𝑔} ⊆ 𝑏
6851cneg 10869 . . . . . . . . . . . . . 14 class -𝑘
6968, 37cfv 6343 . . . . . . . . . . . . 13 class (𝑓‘-𝑘)
7019, 20, 39co 7149 . . . . . . . . . . . . . 14 class (𝑝 + 1)
71 cexp 13434 . . . . . . . . . . . . . 14 class
7270, 68, 71co 7149 . . . . . . . . . . . . 13 class ((𝑝 + 1)↑-𝑘)
7369, 72, 56co 7149 . . . . . . . . . . . 12 class ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
748, 73, 50csu 15042 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
7568, 38cfv 6343 . . . . . . . . . . . . 13 class (𝑔‘-𝑘)
7675, 72, 56co 7149 . . . . . . . . . . . 12 class ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
778, 76, 50csu 15042 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
78 clt 10673 . . . . . . . . . . 11 class <
7974, 77, 78wbr 5052 . . . . . . . . . 10 wff Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
8067, 79wa 399 . . . . . . . . 9 wff ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))
8180, 35, 36copab 5114 . . . . . . . 8 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}
8265, 81cop 4556 . . . . . . 7 class ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩
8382csn 4550 . . . . . 6 class {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}
8463, 83cun 3917 . . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩})
858, 10cxp 5540 . . . . . . . 8 class (ℤ × {0})
8637, 85wceq 1538 . . . . . . 7 wff 𝑓 = (ℤ × {0})
8737ccnv 5541 . . . . . . . . . . 11 class 𝑓
8887, 11cima 5545 . . . . . . . . . 10 class (𝑓 “ (ℤ ∖ {0}))
89 cr 10534 . . . . . . . . . 10 class
9088, 89, 78cinf 8902 . . . . . . . . 9 class inf((𝑓 “ (ℤ ∖ {0})), ℝ, < )
9190cneg 10869 . . . . . . . 8 class -inf((𝑓 “ (ℤ ∖ {0})), ℝ, < )
9219, 91, 71co 7149 . . . . . . 7 class (𝑝↑-inf((𝑓 “ (ℤ ∖ {0})), ℝ, < ))
9386, 9, 92cif 4450 . . . . . 6 class if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((𝑓 “ (ℤ ∖ {0})), ℝ, < )))
9435, 31, 93cmpt 5132 . . . . 5 class (𝑓𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((𝑓 “ (ℤ ∖ {0})), ℝ, < ))))
95 ctng 23188 . . . . 5 class toNrmGrp
9684, 94, 95co 7149 . . . 4 class (({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((𝑓 “ (ℤ ∖ {0})), ℝ, < )))))
974, 27, 96csb 3866 . . 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 5132 . 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 1538 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