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

Definition df-qpOLD 30808
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 30807 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
StepHypRef Expression
1 cqpOLD 30798 . 2 class QpOLD
2 vp . . 3 setvar 𝑝
3 cprime 15223 . . 3 class
4 vb . . . 4 setvar 𝑏
5 vh . . . . . . . . . 10 setvar
65cv 1474 . . . . . . . . 9 class
76ccnv 5037 . . . . . . . 8 class
8 cz 11254 . . . . . . . . 9 class
9 cc0 9815 . . . . . . . . . 10 class 0
109csn 4125 . . . . . . . . 9 class {0}
118, 10cdif 3537 . . . . . . . 8 class (ℤ ∖ {0})
127, 11cima 5041 . . . . . . 7 class ( “ (ℤ ∖ {0}))
13 vx . . . . . . . 8 setvar 𝑥
1413cv 1474 . . . . . . 7 class 𝑥
1512, 14wss 3540 . . . . . 6 wff ( “ (ℤ ∖ {0})) ⊆ 𝑥
16 cuz 11563 . . . . . . 7 class
1716crn 5039 . . . . . 6 class ran ℤ
1815, 13, 17wrex 2897 . . . . 5 wff 𝑥 ∈ ran ℤ( “ (ℤ ∖ {0})) ⊆ 𝑥
192cv 1474 . . . . . . . 8 class 𝑝
20 c1 9816 . . . . . . . 8 class 1
21 cmin 10145 . . . . . . . 8 class
2219, 20, 21co 6549 . . . . . . 7 class (𝑝 − 1)
23 cfz 12197 . . . . . . 7 class ...
249, 22, 23co 6549 . . . . . 6 class (0...(𝑝 − 1))
25 cmap 7744 . . . . . 6 class 𝑚
268, 24, 25co 6549 . . . . 5 class (ℤ ↑𝑚 (0...(𝑝 − 1)))
2718, 5, 26crab 2900 . . . 4 class { ∈ (ℤ ↑𝑚 (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ( “ (ℤ ∖ {0})) ⊆ 𝑥}
28 cnx 15692 . . . . . . . . 9 class ndx
29 cbs 15695 . . . . . . . . 9 class Base
3028, 29cfv 5804 . . . . . . . 8 class (Base‘ndx)
314cv 1474 . . . . . . . 8 class 𝑏
3230, 31cop 4131 . . . . . . 7 class ⟨(Base‘ndx), 𝑏
33 cplusg 15768 . . . . . . . . 9 class +g
3428, 33cfv 5804 . . . . . . . 8 class (+g‘ndx)
35 vf . . . . . . . . 9 setvar 𝑓
36 vg . . . . . . . . 9 setvar 𝑔
3735cv 1474 . . . . . . . . . . 11 class 𝑓
3836cv 1474 . . . . . . . . . . 11 class 𝑔
39 caddc 9818 . . . . . . . . . . . 12 class +
4039cof 6793 . . . . . . . . . . 11 class 𝑓 +
4137, 38, 40co 6549 . . . . . . . . . 10 class (𝑓𝑓 + 𝑔)
42 crqp 30796 . . . . . . . . . . 11 class /Qp
4319, 42cfv 5804 . . . . . . . . . 10 class (/Qp‘𝑝)
4441, 43cfv 5804 . . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑓𝑓 + 𝑔))
4535, 36, 31, 31, 44cmpt2 6551 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓𝑓 + 𝑔)))
4634, 45cop 4131 . . . . . . 7 class ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓𝑓 + 𝑔)))⟩
47 cmulr 15769 . . . . . . . . 9 class .r
4828, 47cfv 5804 . . . . . . . 8 class (.r‘ndx)
49 vn . . . . . . . . . . 11 setvar 𝑛
50 vk . . . . . . . . . . . . . . 15 setvar 𝑘
5150cv 1474 . . . . . . . . . . . . . 14 class 𝑘
5251, 37cfv 5804 . . . . . . . . . . . . 13 class (𝑓𝑘)
5349cv 1474 . . . . . . . . . . . . . . 15 class 𝑛
5453, 51, 21co 6549 . . . . . . . . . . . . . 14 class (𝑛𝑘)
5554, 38cfv 5804 . . . . . . . . . . . . 13 class (𝑔‘(𝑛𝑘))
56 cmul 9820 . . . . . . . . . . . . 13 class ·
5752, 55, 56co 6549 . . . . . . . . . . . 12 class ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))
588, 57, 50csu 14264 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))
5949, 8, 58cmpt 4643 . . . . . . . . . 10 class (𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))
6059, 43cfv 5804 . . . . . . . . 9 class ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘)))))
6135, 36, 31, 31, 60cmpt2 6551 . . . . . . . 8 class (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))
6248, 61cop 4131 . . . . . . 7 class ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩
6332, 46, 62ctp 4129 . . . . . 6 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩}
64 cple 15775 . . . . . . . . 9 class le
6528, 64cfv 5804 . . . . . . . 8 class (le‘ndx)
6637, 38cpr 4127 . . . . . . . . . . 11 class {𝑓, 𝑔}
6766, 31wss 3540 . . . . . . . . . 10 wff {𝑓, 𝑔} ⊆ 𝑏
6851cneg 10146 . . . . . . . . . . . . . 14 class -𝑘
6968, 37cfv 5804 . . . . . . . . . . . . 13 class (𝑓‘-𝑘)
7019, 20, 39co 6549 . . . . . . . . . . . . . 14 class (𝑝 + 1)
71 cexp 12722 . . . . . . . . . . . . . 14 class
7270, 68, 71co 6549 . . . . . . . . . . . . 13 class ((𝑝 + 1)↑-𝑘)
7369, 72, 56co 6549 . . . . . . . . . . . 12 class ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
748, 73, 50csu 14264 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘))
7568, 38cfv 5804 . . . . . . . . . . . . 13 class (𝑔‘-𝑘)
7675, 72, 56co 6549 . . . . . . . . . . . 12 class ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
778, 76, 50csu 14264 . . . . . . . . . . 11 class Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
78 clt 9953 . . . . . . . . . . 11 class <
7974, 77, 78wbr 4583 . . . . . . . . . 10 wff Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))
8067, 79wa 383 . . . . . . . . 9 wff ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))
8180, 35, 36copab 4642 . . . . . . . 8 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}
8265, 81cop 4131 . . . . . . 7 class ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩
8382csn 4125 . . . . . 6 class {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}
8463, 83cun 3538 . . . . 5 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩})
858, 10cxp 5036 . . . . . . . 8 class (ℤ × {0})
8637, 85wceq 1475 . . . . . . 7 wff 𝑓 = (ℤ × {0})
8737ccnv 5037 . . . . . . . . . . 11 class 𝑓
8887, 11cima 5041 . . . . . . . . . 10 class (𝑓 “ (ℤ ∖ {0}))
89 cr 9814 . . . . . . . . . 10 class
9078ccnv 5037 . . . . . . . . . 10 class <
9188, 89, 90csup 8229 . . . . . . . . 9 class sup((𝑓 “ (ℤ ∖ {0})), ℝ, < )
9291cneg 10146 . . . . . . . 8 class -sup((𝑓 “ (ℤ ∖ {0})), ℝ, < )
9319, 92, 71co 6549 . . . . . . 7 class (𝑝↑-sup((𝑓 “ (ℤ ∖ {0})), ℝ, < ))
9486, 9, 93cif 4036 . . . . . 6 class if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((𝑓 “ (ℤ ∖ {0})), ℝ, < )))
9535, 31, 94cmpt 4643 . . . . 5 class (𝑓𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((𝑓 “ (ℤ ∖ {0})), ℝ, < ))))
96 ctng 22193 . . . . 5 class toNrmGrp
9784, 95, 96co 6549 . . . 4 class (({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((𝑓 “ (ℤ ∖ {0})), ℝ, < )))))
984, 27, 97csb 3499 . . 3 class { ∈ (ℤ ↑𝑚 (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ( “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((𝑓 “ (ℤ ∖ {0})), ℝ, < )))))
992, 3, 98cmpt 4643 . 2 class (𝑝 ∈ ℙ ↦ { ∈ (ℤ ↑𝑚 (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ( “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑓𝑓 + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓𝑘) · (𝑔‘(𝑛𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-sup((𝑓 “ (ℤ ∖ {0})), ℝ, < ))))))
1001, 99wceq 1475 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})), ℝ, < ))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator