Metamath Proof Explorer

Definition df-qp

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) (Revised by AV, 10-Oct-2021)

Ref Expression
Assertion 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 oF + 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 inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqp 
 |-  Qp
1 vp 
 |-  p
2 cprime 
 |-  Prime
3 vh 
 |-  h
4 cz 
 |-  ZZ
5 cmap 
 |-  ^m
6 cc0 
 |-  0
7 cfz 
 |-  ...
8 1 cv 
 |-  p
9 cmin 
 |-  -
10 c1 
 |-  1
11 8 10 9 co 
 |-  ( p - 1 )
12 6 11 7 co 
 |-  ( 0 ... ( p - 1 ) )
13 4 12 5 co 
 |-  ( ZZ ^m ( 0 ... ( p - 1 ) ) )
14 vx 
 |-  x
15 cuz 
 |-  ZZ>=
16 15 crn 
 |-  ran ZZ>=
17 3 cv 
 |-  h
18 17 ccnv 
 |-  `' h
19 6 csn 
 |-  { 0 }
20 4 19 cdif 
 |-  ( ZZ \ { 0 } )
21 18 20 cima 
 |-  ( `' h " ( ZZ \ { 0 } ) )
22 14 cv 
 |-  x
23 21 22 wss 
 |-  ( `' h " ( ZZ \ { 0 } ) ) C_ x
24 23 14 16 wrex 
 |-  E. x e. ran ZZ>= ( `' h " ( ZZ \ { 0 } ) ) C_ x
25 24 3 13 crab 
 |-  { h e. ( ZZ ^m ( 0 ... ( p - 1 ) ) ) | E. x e. ran ZZ>= ( `' h " ( ZZ \ { 0 } ) ) C_ x }
26 vb 
 |-  b
27 cbs 
 |-  Base
28 cnx 
 |-  ndx
29 28 27 cfv 
 |-  ( Base ` ndx )
30 26 cv 
 |-  b
31 29 30 cop 
 |-  <. ( Base ` ndx ) , b >.
32 cplusg 
 |-  +g
33 28 32 cfv 
 |-  ( +g ` ndx )
34 vf 
 |-  f
35 vg 
 |-  g
36 crqp 
 |-  /Qp
37 8 36 cfv 
 |-  ( /Qp ` p )
38 34 cv 
 |-  f
39 caddc 
 |-  +
40 39 cof 
 |-  oF +
41 35 cv 
 |-  g
42 38 41 40 co 
 |-  ( f oF + g )
43 42 37 cfv 
 |-  ( ( /Qp ` p ) ` ( f oF + g ) )
44 34 35 30 30 43 cmpo 
 |-  ( f e. b , g e. b |-> ( ( /Qp ` p ) ` ( f oF + g ) ) )
45 33 44 cop 
 |-  <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( ( /Qp ` p ) ` ( f oF + g ) ) ) >.
46 cmulr 
 |-  .r
47 28 46 cfv 
 |-  ( .r ` ndx )
48 vn 
 |-  n
49 vk 
 |-  k
50 49 cv 
 |-  k
51 50 38 cfv 
 |-  ( f ` k )
52 cmul 
 |-  x.
53 48 cv 
 |-  n
54 53 50 9 co 
 |-  ( n - k )
55 54 41 cfv 
 |-  ( g ` ( n - k ) )
56 51 55 52 co 
 |-  ( ( f ` k ) x. ( g ` ( n - k ) ) )
57 4 56 49 csu 
 |-  sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) )
58 48 4 57 cmpt 
 |-  ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) )
59 58 37 cfv 
 |-  ( ( /Qp ` p ) ` ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) ) )
60 34 35 30 30 59 cmpo 
 |-  ( f e. b , g e. b |-> ( ( /Qp ` p ) ` ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) ) ) )
61 47 60 cop 
 |-  <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( ( /Qp ` p ) ` ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) ) ) ) >.
62 31 45 61 ctp 
 |-  { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( ( /Qp ` p ) ` ( f oF + g ) ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( ( /Qp ` p ) ` ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) ) ) ) >. }
63 cple 
 |-  le
64 28 63 cfv 
 |-  ( le ` ndx )
65 38 41 cpr 
 |-  { f , g }
66 65 30 wss 
 |-  { f , g } C_ b
67 50 cneg 
 |-  -u k
68 67 38 cfv 
 |-  ( f ` -u k )
69 8 10 39 co 
 |-  ( p + 1 )
70 cexp 
 |-  ^
71 69 67 70 co 
 |-  ( ( p + 1 ) ^ -u k )
72 68 71 52 co 
 |-  ( ( f ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
73 4 72 49 csu 
 |-  sum_ k e. ZZ ( ( f ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
74 clt 
 |-  <
75 67 41 cfv 
 |-  ( g ` -u k )
76 75 71 52 co 
 |-  ( ( g ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
77 4 76 49 csu 
 |-  sum_ k e. ZZ ( ( g ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
78 73 77 74 wbr 
 |-  sum_ k e. ZZ ( ( f ` -u k ) x. ( ( p + 1 ) ^ -u k ) ) < sum_ k e. ZZ ( ( g ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
79 66 78 wa 
 |-  ( { 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 ) ) )
80 79 34 35 copab 
 |-  { <. 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 ) ) ) }
81 64 80 cop 
 |-  <. ( 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 ) ) ) } >.
82 81 csn 
 |-  { <. ( 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 ) ) ) } >. }
83 62 82 cun 
 |-  ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( ( /Qp ` p ) ` ( f oF + 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 ) ) ) } >. } )
84 ctng 
 |-  toNrmGrp
85 4 19 cxp 
 |-  ( ZZ X. { 0 } )
86 38 85 wceq 
 |-  f = ( ZZ X. { 0 } )
87 38 ccnv 
 |-  `' f
88 87 20 cima 
 |-  ( `' f " ( ZZ \ { 0 } ) )
89 cr 
 |-  RR
90 88 89 74 cinf 
 |-  inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < )
91 90 cneg 
 |-  -u inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < )
92 8 91 70 co 
 |-  ( p ^ -u inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) )
93 86 6 92 cif 
 |-  if ( f = ( ZZ X. { 0 } ) , 0 , ( p ^ -u inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) )
94 34 30 93 cmpt 
 |-  ( f e. b |-> if ( f = ( ZZ X. { 0 } ) , 0 , ( p ^ -u inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) )
95 83 94 84 co 
 |-  ( ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( ( /Qp ` p ) ` ( f oF + 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 inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) )
96 26 25 95 csb 
 |-  [_ { 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 oF + 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 inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) )
97 1 2 96 cmpt 
 |-  ( 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 oF + 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 inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) ) )
98 0 97 wceq 
 |-  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 oF + 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 inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) ) )