Definition df-qp 31553

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.)

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 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 ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) ) )

Distinct variable group:   f, b, g, h, k, n, p, x

Detailed syntax breakdown of Definition df-qp

Step	Hyp	Ref	Expression
1		cqp 31543	. 2 class Qp
2		vp	. . 3 setvar p
3		cprime 15385	. . 3 class Prime
4		vb	. . . 4 setvar b
5		vh	. . . . . . . . . 10 setvar h
6	5	cv 1482	. . . . . . . . 9 class h
7	6	ccnv 5113	. . . . . . . 8 class `' h
8		cz 11377	. . . . . . . . 9 class ZZ
9		cc0 9936	. . . . . . . . . 10 class 0
10	9	csn 4177	. . . . . . . . 9 class { 0 }
11	8, 10	cdif 3571	. . . . . . . 8 class ( ZZ \ { 0 } )
12	7, 11	cima 5117	. . . . . . 7 class ( `' h " ( ZZ \ { 0 } ) )
13		vx	. . . . . . . 8 setvar x
14	13	cv 1482	. . . . . . 7 class x
15	12, 14	wss 3574	. . . . . 6 wff ( `' h " ( ZZ \ { 0 } ) ) C_ x
16		cuz 11687	. . . . . . 7 class ZZ>=
17	16	crn 5115	. . . . . 6 class ran ZZ>=
18	15, 13, 17	wrex 2913	. . . . 5 wff E. x e. ran ZZ>= ( `' h " ( ZZ \ { 0 } ) ) C_ x
19	2	cv 1482	. . . . . . . 8 class p
20		c1 9937	. . . . . . . 8 class 1
21		cmin 10266	. . . . . . . 8 class -
22	19, 20, 21	co 6650	. . . . . . 7 class ( p - 1 )
23		cfz 12326	. . . . . . 7 class ...
24	9, 22, 23	co 6650	. . . . . 6 class ( 0 ... ( p - 1 ) )
25		cmap 7857	. . . . . 6 class ^m
26	8, 24, 25	co 6650	. . . . 5 class ( ZZ ^m ( 0 ... ( p - 1 ) ) )
27	18, 5, 26	crab 2916	. . . 4 class { h e. ( ZZ ^m ( 0 ... ( p - 1 ) ) ) | E. x e. ran ZZ>= ( `' h " ( ZZ \ { 0 } ) ) C_ x }
28		cnx 15854	. . . . . . . . 9 class ndx
29		cbs 15857	. . . . . . . . 9 class Base
30	28, 29	cfv 5888	. . . . . . . 8 class ( Base ` ndx )
31	4	cv 1482	. . . . . . . 8 class b
32	30, 31	cop 4183	. . . . . . 7 class <. ( Base ` ndx ) , b >.
33		cplusg 15941	. . . . . . . . 9 class +g
34	28, 33	cfv 5888	. . . . . . . 8 class ( +g ` ndx )
35		vf	. . . . . . . . 9 setvar f
36		vg	. . . . . . . . 9 setvar g
37	35	cv 1482	. . . . . . . . . . 11 class f
38	36	cv 1482	. . . . . . . . . . 11 class g
39		caddc 9939	. . . . . . . . . . . 12 class +
40	39	cof 6895	. . . . . . . . . . 11 class oF +
41	37, 38, 40	co 6650	. . . . . . . . . 10 class ( f oF + g )
42		crqp 31542	. . . . . . . . . . 11 class /Qp
43	19, 42	cfv 5888	. . . . . . . . . 10 class (/Qp ` p )
44	41, 43	cfv 5888	. . . . . . . . 9 class ( (/Qp ` p ) ` ( f oF + g ) )
45	35, 36, 31, 31, 44	cmpt2 6652	. . . . . . . 8 class ( f e. b , g e. b |-> ( (/Qp ` p ) ` ( f oF + g ) ) )
46	34, 45	cop 4183	. . . . . . 7 class <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( (/Qp ` p ) ` ( f oF + g ) ) ) >.
47		cmulr 15942	. . . . . . . . 9 class .r
48	28, 47	cfv 5888	. . . . . . . 8 class ( .r ` ndx )
49		vn	. . . . . . . . . . 11 setvar n
50		vk	. . . . . . . . . . . . . . 15 setvar k
51	50	cv 1482	. . . . . . . . . . . . . 14 class k
52	51, 37	cfv 5888	. . . . . . . . . . . . 13 class ( f ` k )
53	49	cv 1482	. . . . . . . . . . . . . . 15 class n
54	53, 51, 21	co 6650	. . . . . . . . . . . . . 14 class ( n - k )
55	54, 38	cfv 5888	. . . . . . . . . . . . 13 class ( g ` ( n - k ) )
56		cmul 9941	. . . . . . . . . . . . 13 class x.
57	52, 55, 56	co 6650	. . . . . . . . . . . 12 class ( ( f ` k ) x. ( g ` ( n - k ) ) )
58	8, 57, 50	csu 14416	. . . . . . . . . . 11 class sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) )
59	49, 8, 58	cmpt 4729	. . . . . . . . . 10 class ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) )
60	59, 43	cfv 5888	. . . . . . . . 9 class ( (/Qp ` p ) ` ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) ) )
61	35, 36, 31, 31, 60	cmpt2 6652	. . . . . . . 8 class ( f e. b , g e. b |-> ( (/Qp ` p ) ` ( n e. ZZ |-> sum_ k e. ZZ ( ( f ` k ) x. ( g ` ( n - k ) ) ) ) ) )
62	48, 61	cop 4183	. . . . . . 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 ) ) ) ) ) ) >.
63	32, 46, 62	ctp 4181	. . . . . 6 class { <. ( 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 ) ) ) ) ) ) >. }
64		cple 15948	. . . . . . . . 9 class le
65	28, 64	cfv 5888	. . . . . . . 8 class ( le ` ndx )
66	37, 38	cpr 4179	. . . . . . . . . . 11 class { f , g }
67	66, 31	wss 3574	. . . . . . . . . 10 wff { f , g } C_ b
68	51	cneg 10267	. . . . . . . . . . . . . 14 class -u k
69	68, 37	cfv 5888	. . . . . . . . . . . . 13 class ( f ` -u k )
70	19, 20, 39	co 6650	. . . . . . . . . . . . . 14 class ( p + 1 )
71		cexp 12860	. . . . . . . . . . . . . 14 class ^
72	70, 68, 71	co 6650	. . . . . . . . . . . . 13 class ( ( p + 1 ) ^ -u k )
73	69, 72, 56	co 6650	. . . . . . . . . . . 12 class ( ( f ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
74	8, 73, 50	csu 14416	. . . . . . . . . . 11 class sum_ k e. ZZ ( ( f ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
75	68, 38	cfv 5888	. . . . . . . . . . . . 13 class ( g ` -u k )
76	75, 72, 56	co 6650	. . . . . . . . . . . 12 class ( ( g ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
77	8, 76, 50	csu 14416	. . . . . . . . . . 11 class sum_ k e. ZZ ( ( g ` -u k ) x. ( ( p + 1 ) ^ -u k ) )
78		clt 10074	. . . . . . . . . . 11 class <
79	74, 77, 78	wbr 4653	. . . . . . . . . 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 ) )
80	67, 79	wa 384	. . . . . . . . 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 ) ) )
81	80, 35, 36	copab 4712	. . . . . . . 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 ) ) ) }
82	65, 81	cop 4183	. . . . . . 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 ) ) ) } >.
83	82	csn 4177	. . . . . 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 ) ) ) } >. }
84	63, 83	cun 3572	. . . . 5 class ( { <. ( 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 ) ) ) } >. } )
85	8, 10	cxp 5112	. . . . . . . 8 class ( ZZ X. { 0 } )
86	37, 85	wceq 1483	. . . . . . 7 wff f = ( ZZ X. { 0 } )
87	37	ccnv 5113	. . . . . . . . . . 11 class `' f
88	87, 11	cima 5117	. . . . . . . . . 10 class ( `' f " ( ZZ \ { 0 } ) )
89		cr 9935	. . . . . . . . . 10 class RR
90	88, 89, 78	cinf 8347	. . . . . . . . 9 class inf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < )
91	90	cneg 10267	. . . . . . . 8 class -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < )
92	19, 91, 71	co 6650	. . . . . . 7 class ( p ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) )
93	86, 9, 92	cif 4086	. . . . . 6 class if ( f = ( ZZ X. { 0 } ) , 0 , ( p ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) )
94	35, 31, 93	cmpt 4729	. . . . 5 class ( f e. b |-> if ( f = ( ZZ X. { 0 } ) , 0 , ( p ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) )
95		ctng 22383	. . . . 5 class toNrmGrp
96	84, 94, 95	co 6650	. . . 4 class ( ( { <. ( 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 ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) )
97	4, 27, 96	csb 3533	. . 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 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 ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) )
98	2, 3, 97	cmpt 4729	. 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 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 ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) ) )
99	1, 98	wceq 1483	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 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 ^ -uinf ( ( `' f " ( ZZ \ { 0 } ) ) , RR , < ) ) ) ) ) )

This definition is referenced by: (None)