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 34641
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 34632 . 2 class Qp
2 vp . . 3 setvar 𝑝
3 cprime 16607 . . 3 class β„™
4 vb . . . 4 setvar 𝑏
5 vh . . . . . . . . . 10 setvar β„Ž
65cv 1540 . . . . . . . . 9 class β„Ž
76ccnv 5675 . . . . . . . 8 class β—‘β„Ž
8 cz 12557 . . . . . . . . 9 class β„€
9 cc0 11109 . . . . . . . . . 10 class 0
109csn 4628 . . . . . . . . 9 class {0}
118, 10cdif 3945 . . . . . . . 8 class (β„€ βˆ– {0})
127, 11cima 5679 . . . . . . 7 class (β—‘β„Ž β€œ (β„€ βˆ– {0}))
13 vx . . . . . . . 8 setvar π‘₯
1413cv 1540 . . . . . . 7 class π‘₯
1512, 14wss 3948 . . . . . 6 wff (β—‘β„Ž β€œ (β„€ βˆ– {0})) βŠ† π‘₯
16 cuz 12821 . . . . . . 7 class β„€β‰₯
1716crn 5677 . . . . . 6 class ran β„€β‰₯
1815, 13, 17wrex 3070 . . . . 5 wff βˆƒπ‘₯ ∈ ran β„€β‰₯(β—‘β„Ž β€œ (β„€ βˆ– {0})) βŠ† π‘₯
192cv 1540 . . . . . . . 8 class 𝑝
20 c1 11110 . . . . . . . 8 class 1
21 cmin 11443 . . . . . . . 8 class βˆ’
2219, 20, 21co 7408 . . . . . . 7 class (𝑝 βˆ’ 1)
23 cfz 13483 . . . . . . 7 class ...
249, 22, 23co 7408 . . . . . 6 class (0...(𝑝 βˆ’ 1))
25 cmap 8819 . . . . . 6 class ↑m
268, 24, 25co 7408 . . . . 5 class (β„€ ↑m (0...(𝑝 βˆ’ 1)))
2718, 5, 26crab 3432 . . . 4 class {β„Ž ∈ (β„€ ↑m (0...(𝑝 βˆ’ 1))) ∣ βˆƒπ‘₯ ∈ ran β„€β‰₯(β—‘β„Ž β€œ (β„€ βˆ– {0})) βŠ† π‘₯}
28 cnx 17125 . . . . . . . . 9 class ndx
29 cbs 17143 . . . . . . . . 9 class Base
3028, 29cfv 6543 . . . . . . . 8 class (Baseβ€˜ndx)
314cv 1540 . . . . . . . 8 class 𝑏
3230, 31cop 4634 . . . . . . 7 class ⟨(Baseβ€˜ndx), π‘βŸ©
33 cplusg 17196 . . . . . . . . 9 class +g
3428, 33cfv 6543 . . . . . . . 8 class (+gβ€˜ndx)
35 vf . . . . . . . . 9 setvar 𝑓
36 vg . . . . . . . . 9 setvar 𝑔
3735cv 1540 . . . . . . . . . . 11 class 𝑓
3836cv 1540 . . . . . . . . . . 11 class 𝑔
39 caddc 11112 . . . . . . . . . . . 12 class +
4039cof 7667 . . . . . . . . . . 11 class ∘f +
4137, 38, 40co 7408 . . . . . . . . . 10 class (𝑓 ∘f + 𝑔)
42 crqp 34631 . . . . . . . . . . 11 class /Qp
4319, 42cfv 6543 . . . . . . . . . 10 class (/Qpβ€˜π‘)
4441, 43cfv 6543 . . . . . . . . 9 class ((/Qpβ€˜π‘)β€˜(𝑓 ∘f + 𝑔))
4535, 36, 31, 31, 44cmpo 7410 . . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑓 ∘f + 𝑔)))
4634, 45cop 4634 . . . . . . 7 class ⟨(+gβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑓 ∘f + 𝑔)))⟩
47 cmulr 17197 . . . . . . . . 9 class .r
4828, 47cfv 6543 . . . . . . . 8 class (.rβ€˜ndx)
49 vn . . . . . . . . . . 11 setvar 𝑛
50 vk . . . . . . . . . . . . . . 15 setvar π‘˜
5150cv 1540 . . . . . . . . . . . . . 14 class π‘˜
5251, 37cfv 6543 . . . . . . . . . . . . 13 class (π‘“β€˜π‘˜)
5349cv 1540 . . . . . . . . . . . . . . 15 class 𝑛
5453, 51, 21co 7408 . . . . . . . . . . . . . 14 class (𝑛 βˆ’ π‘˜)
5554, 38cfv 6543 . . . . . . . . . . . . 13 class (π‘”β€˜(𝑛 βˆ’ π‘˜))
56 cmul 11114 . . . . . . . . . . . . 13 class Β·
5752, 55, 56co 7408 . . . . . . . . . . . 12 class ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜)))
588, 57, 50csu 15631 . . . . . . . . . . 11 class Ξ£π‘˜ ∈ β„€ ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜)))
5949, 8, 58cmpt 5231 . . . . . . . . . 10 class (𝑛 ∈ β„€ ↦ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜))))
6059, 43cfv 6543 . . . . . . . . 9 class ((/Qpβ€˜π‘)β€˜(𝑛 ∈ β„€ ↦ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜)))))
6135, 36, 31, 31, 60cmpo 7410 . . . . . . . 8 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑛 ∈ β„€ ↦ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜))))))
6248, 61cop 4634 . . . . . . 7 class ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑛 ∈ β„€ ↦ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜))))))⟩
6332, 46, 62ctp 4632 . . . . . 6 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑓 ∘f + 𝑔)))⟩, ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑛 ∈ β„€ ↦ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜))))))⟩}
64 cple 17203 . . . . . . . . 9 class le
6528, 64cfv 6543 . . . . . . . 8 class (leβ€˜ndx)
6637, 38cpr 4630 . . . . . . . . . . 11 class {𝑓, 𝑔}
6766, 31wss 3948 . . . . . . . . . 10 wff {𝑓, 𝑔} βŠ† 𝑏
6851cneg 11444 . . . . . . . . . . . . . 14 class -π‘˜
6968, 37cfv 6543 . . . . . . . . . . . . 13 class (π‘“β€˜-π‘˜)
7019, 20, 39co 7408 . . . . . . . . . . . . . 14 class (𝑝 + 1)
71 cexp 14026 . . . . . . . . . . . . . 14 class ↑
7270, 68, 71co 7408 . . . . . . . . . . . . 13 class ((𝑝 + 1)↑-π‘˜)
7369, 72, 56co 7408 . . . . . . . . . . . 12 class ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜))
748, 73, 50csu 15631 . . . . . . . . . . 11 class Ξ£π‘˜ ∈ β„€ ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜))
7568, 38cfv 6543 . . . . . . . . . . . . 13 class (π‘”β€˜-π‘˜)
7675, 72, 56co 7408 . . . . . . . . . . . 12 class ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜))
778, 76, 50csu 15631 . . . . . . . . . . 11 class Ξ£π‘˜ ∈ β„€ ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜))
78 clt 11247 . . . . . . . . . . 11 class <
7974, 77, 78wbr 5148 . . . . . . . . . 10 wff Ξ£π‘˜ ∈ β„€ ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)) < Ξ£π‘˜ ∈ β„€ ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜))
8067, 79wa 396 . . . . . . . . 9 wff ({𝑓, 𝑔} βŠ† 𝑏 ∧ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)) < Ξ£π‘˜ ∈ β„€ ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)))
8180, 35, 36copab 5210 . . . . . . . 8 class {βŸ¨π‘“, π‘”βŸ© ∣ ({𝑓, 𝑔} βŠ† 𝑏 ∧ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)) < Ξ£π‘˜ ∈ β„€ ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)))}
8265, 81cop 4634 . . . . . . 7 class ⟨(leβ€˜ndx), {βŸ¨π‘“, π‘”βŸ© ∣ ({𝑓, 𝑔} βŠ† 𝑏 ∧ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)) < Ξ£π‘˜ ∈ β„€ ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)))}⟩
8382csn 4628 . . . . . 6 class {⟨(leβ€˜ndx), {βŸ¨π‘“, π‘”βŸ© ∣ ({𝑓, 𝑔} βŠ† 𝑏 ∧ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)) < Ξ£π‘˜ ∈ β„€ ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)))}⟩}
8463, 83cun 3946 . . . . 5 class ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑓 ∘f + 𝑔)))⟩, ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑛 ∈ β„€ ↦ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜))))))⟩} βˆͺ {⟨(leβ€˜ndx), {βŸ¨π‘“, π‘”βŸ© ∣ ({𝑓, 𝑔} βŠ† 𝑏 ∧ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)) < Ξ£π‘˜ ∈ β„€ ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)))}⟩})
858, 10cxp 5674 . . . . . . . 8 class (β„€ Γ— {0})
8637, 85wceq 1541 . . . . . . 7 wff 𝑓 = (β„€ Γ— {0})
8737ccnv 5675 . . . . . . . . . . 11 class ◑𝑓
8887, 11cima 5679 . . . . . . . . . 10 class (◑𝑓 β€œ (β„€ βˆ– {0}))
89 cr 11108 . . . . . . . . . 10 class ℝ
9088, 89, 78cinf 9435 . . . . . . . . 9 class inf((◑𝑓 β€œ (β„€ βˆ– {0})), ℝ, < )
9190cneg 11444 . . . . . . . 8 class -inf((◑𝑓 β€œ (β„€ βˆ– {0})), ℝ, < )
9219, 91, 71co 7408 . . . . . . 7 class (𝑝↑-inf((◑𝑓 β€œ (β„€ βˆ– {0})), ℝ, < ))
9386, 9, 92cif 4528 . . . . . 6 class if(𝑓 = (β„€ Γ— {0}), 0, (𝑝↑-inf((◑𝑓 β€œ (β„€ βˆ– {0})), ℝ, < )))
9435, 31, 93cmpt 5231 . . . . 5 class (𝑓 ∈ 𝑏 ↦ if(𝑓 = (β„€ Γ— {0}), 0, (𝑝↑-inf((◑𝑓 β€œ (β„€ βˆ– {0})), ℝ, < ))))
95 ctng 24086 . . . . 5 class toNrmGrp
9684, 94, 95co 7408 . . . 4 class (({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑓 ∘f + 𝑔)))⟩, ⟨(.rβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qpβ€˜π‘)β€˜(𝑛 ∈ β„€ ↦ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜π‘˜) Β· (π‘”β€˜(𝑛 βˆ’ π‘˜))))))⟩} βˆͺ {⟨(leβ€˜ndx), {βŸ¨π‘“, π‘”βŸ© ∣ ({𝑓, 𝑔} βŠ† 𝑏 ∧ Ξ£π‘˜ ∈ β„€ ((π‘“β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)) < Ξ£π‘˜ ∈ β„€ ((π‘”β€˜-π‘˜) Β· ((𝑝 + 1)↑-π‘˜)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (β„€ Γ— {0}), 0, (𝑝↑-inf((◑𝑓 β€œ (β„€ βˆ– {0})), ℝ, < )))))
974, 27, 96csb 3893 . . 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 5231 . 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 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})), ℝ, < ))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator