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

Definition df-qp 24003
Description: Define the  p-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.)
Assertion
Ref Expression
df-qp  |- Qp  =  ( p  e.  Prime  |->  [_ {
h  e.  ( ZZ 
^m  ( 0 ... ( p  -  1 ) ) )  |  E. x  e.  ran  ZZ>= ( `' h " ( ZZ 
\  { 0 } ) )  C_  x }  /  b ]_ (
( { <. ( Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( (/Qp `  p
) `  ( f  o F  +  g
) ) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp
`  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) ) ) >. }  u.  { <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
>. } ) toNrmGrp  ( f  e.  b  |->  if ( f  =  ( ZZ 
X.  { 0 } ) ,  0 ,  ( p ^ -u sup ( ( `' f
" ( ZZ  \  { 0 } ) ) ,  RR ,  `'  <  ) ) ) ) ) )
Distinct variable group:    f, b, g, h, k, n, p, x

Detailed syntax breakdown of Definition df-qp
StepHypRef Expression
1 cqp 23994 . 2  class Qp
2 vp . . 3  set  p
3 cprime 12774 . . 3  class  Prime
4 vb . . . 4  set  b
5 vh . . . . . . . . . 10  set  h
65cv 1631 . . . . . . . . 9  class  h
76ccnv 4704 . . . . . . . 8  class  `' h
8 cz 10040 . . . . . . . . 9  class  ZZ
9 cc0 8753 . . . . . . . . . 10  class  0
109csn 3653 . . . . . . . . 9  class  { 0 }
118, 10cdif 3162 . . . . . . . 8  class  ( ZZ 
\  { 0 } )
127, 11cima 4708 . . . . . . 7  class  ( `' h " ( ZZ 
\  { 0 } ) )
13 vx . . . . . . . 8  set  x
1413cv 1631 . . . . . . 7  class  x
1512, 14wss 3165 . . . . . 6  wff  ( `' h " ( ZZ 
\  { 0 } ) )  C_  x
16 cuz 10246 . . . . . . 7  class  ZZ>=
1716crn 4706 . . . . . 6  class  ran  ZZ>=
1815, 13, 17wrex 2557 . . . . 5  wff  E. x  e.  ran  ZZ>= ( `' h " ( ZZ  \  {
0 } ) ) 
C_  x
192cv 1631 . . . . . . . 8  class  p
20 c1 8754 . . . . . . . 8  class  1
21 cmin 9053 . . . . . . . 8  class  -
2219, 20, 21co 5874 . . . . . . 7  class  ( p  -  1 )
23 cfz 10798 . . . . . . 7  class  ...
249, 22, 23co 5874 . . . . . 6  class  ( 0 ... ( p  - 
1 ) )
25 cmap 6788 . . . . . 6  class  ^m
268, 24, 25co 5874 . . . . 5  class  ( ZZ 
^m  ( 0 ... ( p  -  1 ) ) )
2718, 5, 26crab 2560 . . . 4  class  { h  e.  ( ZZ  ^m  (
0 ... ( p  - 
1 ) ) )  |  E. x  e. 
ran  ZZ>= ( `' h " ( ZZ  \  {
0 } ) ) 
C_  x }
28 cnx 13161 . . . . . . . . 9  class  ndx
29 cbs 13164 . . . . . . . . 9  class  Base
3028, 29cfv 5271 . . . . . . . 8  class  ( Base `  ndx )
314cv 1631 . . . . . . . 8  class  b
3230, 31cop 3656 . . . . . . 7  class  <. ( Base `  ndx ) ,  b >.
33 cplusg 13224 . . . . . . . . 9  class  +g
3428, 33cfv 5271 . . . . . . . 8  class  ( +g  ` 
ndx )
35 vf . . . . . . . . 9  set  f
36 vg . . . . . . . . 9  set  g
3735cv 1631 . . . . . . . . . . 11  class  f
3836cv 1631 . . . . . . . . . . 11  class  g
39 caddc 8756 . . . . . . . . . . . 12  class  +
4039cof 6092 . . . . . . . . . . 11  class  o F  +
4137, 38, 40co 5874 . . . . . . . . . 10  class  ( f  o F  +  g )
42 crqp 23993 . . . . . . . . . . 11  class /Qp
4319, 42cfv 5271 . . . . . . . . . 10  class  (/Qp `  p )
4441, 43cfv 5271 . . . . . . . . 9  class  ( (/Qp
`  p ) `  ( f  o F  +  g ) )
4535, 36, 31, 31, 44cmpt2 5876 . . . . . . . 8  class  ( f  e.  b ,  g  e.  b  |->  ( (/Qp
`  p ) `  ( f  o F  +  g ) ) )
4634, 45cop 3656 . . . . . . 7  class  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( (/Qp `  p
) `  ( f  o F  +  g
) ) ) >.
47 cmulr 13225 . . . . . . . . 9  class  .r
4828, 47cfv 5271 . . . . . . . 8  class  ( .r
`  ndx )
49 vn . . . . . . . . . . 11  set  n
50 vk . . . . . . . . . . . . . . 15  set  k
5150cv 1631 . . . . . . . . . . . . . 14  class  k
5251, 37cfv 5271 . . . . . . . . . . . . 13  class  ( f `
 k )
5349cv 1631 . . . . . . . . . . . . . . 15  class  n
5453, 51, 21co 5874 . . . . . . . . . . . . . 14  class  ( n  -  k )
5554, 38cfv 5271 . . . . . . . . . . . . 13  class  ( g `
 ( n  -  k ) )
56 cmul 8758 . . . . . . . . . . . . 13  class  x.
5752, 55, 56co 5874 . . . . . . . . . . . 12  class  ( ( f `  k )  x.  ( g `  ( n  -  k
) ) )
588, 57, 50csu 12174 . . . . . . . . . . 11  class  sum_ k  e.  ZZ  ( ( f `
 k )  x.  ( g `  (
n  -  k ) ) )
5949, 8, 58cmpt 4093 . . . . . . . . . 10  class  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  ( ( f `
 k )  x.  ( g `  (
n  -  k ) ) ) )
6059, 43cfv 5271 . . . . . . . . 9  class  ( (/Qp
`  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) )
6135, 36, 31, 31, 60cmpt2 5876 . . . . . . . 8  class  ( f  e.  b ,  g  e.  b  |->  ( (/Qp
`  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) ) )
6248, 61cop 3656 . . . . . . 7  class  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( (/Qp `  p
) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  ( ( f `  k )  x.  (
g `  ( n  -  k ) ) ) ) ) )
>.
6332, 46, 62ctp 3655 . . . . . 6  class  { <. (
Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( (/Qp `  p
) `  ( f  o F  +  g
) ) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp
`  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) ) ) >. }
64 cple 13231 . . . . . . . . 9  class  le
6528, 64cfv 5271 . . . . . . . 8  class  ( le
`  ndx )
6637, 38cpr 3654 . . . . . . . . . . 11  class  { f ,  g }
6766, 31wss 3165 . . . . . . . . . 10  wff  { f ,  g }  C_  b
6851cneg 9054 . . . . . . . . . . . . . 14  class  -u k
6968, 37cfv 5271 . . . . . . . . . . . . 13  class  ( f `
 -u k )
7019, 20, 39co 5874 . . . . . . . . . . . . . 14  class  ( p  +  1 )
71 cexp 11120 . . . . . . . . . . . . . 14  class  ^
7270, 68, 71co 5874 . . . . . . . . . . . . 13  class  ( ( p  +  1 ) ^ -u k )
7369, 72, 56co 5874 . . . . . . . . . . . 12  class  ( ( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )
748, 73, 50csu 12174 . . . . . . . . . . 11  class  sum_ k  e.  ZZ  ( ( f `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) )
7568, 38cfv 5271 . . . . . . . . . . . . 13  class  ( g `
 -u k )
7675, 72, 56co 5874 . . . . . . . . . . . 12  class  ( ( g `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )
778, 76, 50csu 12174 . . . . . . . . . . 11  class  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) )
78 clt 8883 . . . . . . . . . . 11  class  <
7974, 77, 78wbr 4039 . . . . . . . . . 10  wff  sum_ k  e.  ZZ  ( ( f `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) )  <  sum_ k  e.  ZZ  (
( g `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )
8067, 79wa 358 . . . . . . . . 9  wff  ( { f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) )
8180, 35, 36copab 4092 . . . . . . . 8  class  { <. f ,  g >.  |  ( { f ,  g }  C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
8265, 81cop 3656 . . . . . . 7  class  <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
>.
8382csn 3653 . . . . . 6  class  { <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
>. }
8463, 83cun 3163 . . . . 5  class  ( {
<. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp `  p ) `  (
f  o F  +  g ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp `  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) ) ) >. }  u.  { <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
>. } )
858, 10cxp 4703 . . . . . . . 8  class  ( ZZ 
X.  { 0 } )
8637, 85wceq 1632 . . . . . . 7  wff  f  =  ( ZZ  X.  {
0 } )
8737ccnv 4704 . . . . . . . . . . 11  class  `' f
8887, 11cima 4708 . . . . . . . . . 10  class  ( `' f " ( ZZ 
\  { 0 } ) )
89 cr 8752 . . . . . . . . . 10  class  RR
9078ccnv 4704 . . . . . . . . . 10  class  `'  <
9188, 89, 90csup 7209 . . . . . . . . 9  class  sup (
( `' f "
( ZZ  \  {
0 } ) ) ,  RR ,  `'  <  )
9291cneg 9054 . . . . . . . 8  class  -u sup ( ( `' f
" ( ZZ  \  { 0 } ) ) ,  RR ,  `'  <  )
9319, 92, 71co 5874 . . . . . . 7  class  ( p ^ -u sup (
( `' f "
( ZZ  \  {
0 } ) ) ,  RR ,  `'  <  ) )
9486, 9, 93cif 3578 . . . . . 6  class  if ( f  =  ( ZZ 
X.  { 0 } ) ,  0 ,  ( p ^ -u sup ( ( `' f
" ( ZZ  \  { 0 } ) ) ,  RR ,  `'  <  ) ) )
9535, 31, 94cmpt 4093 . . . . 5  class  ( f  e.  b  |->  if ( f  =  ( ZZ 
X.  { 0 } ) ,  0 ,  ( p ^ -u sup ( ( `' f
" ( ZZ  \  { 0 } ) ) ,  RR ,  `'  <  ) ) ) )
96 ctng 18117 . . . . 5  class toNrmGrp
9784, 95, 96co 5874 . . . 4  class  ( ( { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp `  p ) `  (
f  o F  +  g ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp `  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) ) ) >. }  u.  { <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
>. } ) toNrmGrp  ( f  e.  b  |->  if ( f  =  ( ZZ 
X.  { 0 } ) ,  0 ,  ( p ^ -u sup ( ( `' f
" ( ZZ  \  { 0 } ) ) ,  RR ,  `'  <  ) ) ) ) )
984, 27, 97csb 3094 . . 3  class  [_ {
h  e.  ( ZZ 
^m  ( 0 ... ( p  -  1 ) ) )  |  E. x  e.  ran  ZZ>= ( `' h " ( ZZ 
\  { 0 } ) )  C_  x }  /  b ]_ (
( { <. ( Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( (/Qp `  p
) `  ( f  o F  +  g
) ) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp
`  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) ) ) >. }  u.  { <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
>. } ) toNrmGrp  ( f  e.  b  |->  if ( f  =  ( ZZ 
X.  { 0 } ) ,  0 ,  ( p ^ -u sup ( ( `' f
" ( ZZ  \  { 0 } ) ) ,  RR ,  `'  <  ) ) ) ) )
992, 3, 98cmpt 4093 . 2  class  ( p  e.  Prime  |->  [_ {
h  e.  ( ZZ 
^m  ( 0 ... ( p  -  1 ) ) )  |  E. x  e.  ran  ZZ>= ( `' h " ( ZZ 
\  { 0 } ) )  C_  x }  /  b ]_ (
( { <. ( Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( (/Qp `  p
) `  ( f  o F  +  g
) ) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp
`  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) ) ) >. }  u.  { <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
>. } ) toNrmGrp  ( f  e.  b  |->  if ( f  =  ( ZZ 
X.  { 0 } ) ,  0 ,  ( p ^ -u sup ( ( `' f
" ( ZZ  \  { 0 } ) ) ,  RR ,  `'  <  ) ) ) ) ) )
1001, 99wceq 1632 1  wff Qp  =  ( p  e.  Prime  |->  [_ {
h  e.  ( ZZ 
^m  ( 0 ... ( p  -  1 ) ) )  |  E. x  e.  ran  ZZ>= ( `' h " ( ZZ 
\  { 0 } ) )  C_  x }  /  b ]_ (
( { <. ( Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( (/Qp `  p
) `  ( f  o F  +  g
) ) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( (/Qp
`  p ) `  ( n  e.  ZZ  |->  sum_ k  e.  ZZ  (
( f `  k
)  x.  ( g `
 ( n  -  k ) ) ) ) ) ) >. }  u.  { <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  b  /\  sum_ k  e.  ZZ  (
( f `  -u k
)  x.  ( ( p  +  1 ) ^ -u k ) )  <  sum_ k  e.  ZZ  ( ( g `
 -u k )  x.  ( ( p  + 
1 ) ^ -u k
) ) ) }
>. } ) toNrmGrp  ( f  e.  b  |->  if ( f  =  ( ZZ 
X.  { 0 } ) ,  0 ,  ( p ^ -u sup ( ( `' f
" ( ZZ  \  { 0 } ) ) ,  RR ,  `'  <  ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator