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 = ( 𝑝 ∈ ℙ ↦ { ∈ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ∣ ∃ 𝑥 ∈ ran ℤ ( “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑏 ( ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) ) } ⟩ } ) toNrmGrp ( 𝑓𝑏 ↦ if ( 𝑓 = ( ℤ × { 0 } ) , 0 , ( 𝑝 ↑ - inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqp Qp
1 vp 𝑝
2 cprime
3 vh
4 cz
5 cmap m
6 cc0 0
7 cfz ...
8 1 cv 𝑝
9 cmin
10 c1 1
11 8 10 9 co ( 𝑝 − 1 )
12 6 11 7 co ( 0 ... ( 𝑝 − 1 ) )
13 4 12 5 co ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) )
14 vx 𝑥
15 cuz
16 15 crn ran ℤ
17 3 cv
18 17 ccnv
19 6 csn { 0 }
20 4 19 cdif ( ℤ ∖ { 0 } )
21 18 20 cima ( “ ( ℤ ∖ { 0 } ) )
22 14 cv 𝑥
23 21 22 wss ( “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥
24 23 14 16 wrex 𝑥 ∈ ran ℤ ( “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥
25 24 3 13 crab { ∈ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ∣ ∃ 𝑥 ∈ ran ℤ ( “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 }
26 vb 𝑏
27 cbs Base
28 cnx ndx
29 28 27 cfv ( Base ‘ ndx )
30 26 cv 𝑏
31 29 30 cop ⟨ ( Base ‘ ndx ) , 𝑏
32 cplusg +g
33 28 32 cfv ( +g ‘ ndx )
34 vf 𝑓
35 vg 𝑔
36 crqp /Qp
37 8 36 cfv ( /Qp ‘ 𝑝 )
38 34 cv 𝑓
39 caddc +
40 39 cof f +
41 35 cv 𝑔
42 38 41 40 co ( 𝑓f + 𝑔 )
43 42 37 cfv ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) )
44 34 35 30 30 43 cmpo ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) ) )
45 33 44 cop ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) ) ) ⟩
46 cmulr .r
47 28 46 cfv ( .r ‘ ndx )
48 vn 𝑛
49 vk 𝑘
50 49 cv 𝑘
51 50 38 cfv ( 𝑓𝑘 )
52 cmul ·
53 48 cv 𝑛
54 53 50 9 co ( 𝑛𝑘 )
55 54 41 cfv ( 𝑔 ‘ ( 𝑛𝑘 ) )
56 51 55 52 co ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) )
57 4 56 49 csu Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) )
58 48 4 57 cmpt ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) )
59 58 37 cfv ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) )
60 34 35 30 30 59 cmpo ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) ) )
61 47 60 cop ⟨ ( .r ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) ) ) ⟩
62 31 45 61 ctp { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) ) ) ⟩ }
63 cple le
64 28 63 cfv ( le ‘ ndx )
65 38 41 cpr { 𝑓 , 𝑔 }
66 65 30 wss { 𝑓 , 𝑔 } ⊆ 𝑏
67 50 cneg - 𝑘
68 67 38 cfv ( 𝑓 ‘ - 𝑘 )
69 8 10 39 co ( 𝑝 + 1 )
70 cexp
71 69 67 70 co ( ( 𝑝 + 1 ) ↑ - 𝑘 )
72 68 71 52 co ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) )
73 4 72 49 csu Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) )
74 clt <
75 67 41 cfv ( 𝑔 ‘ - 𝑘 )
76 75 71 52 co ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) )
77 4 76 49 csu Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) )
78 73 77 74 wbr Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) )
79 66 78 wa ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) )
80 79 34 35 copab { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) ) }
81 64 80 cop ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) ) } ⟩
82 81 csn { ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) ) } ⟩ }
83 62 82 cun ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) ) } ⟩ } )
84 ctng toNrmGrp
85 4 19 cxp ( ℤ × { 0 } )
86 38 85 wceq 𝑓 = ( ℤ × { 0 } )
87 38 ccnv 𝑓
88 87 20 cima ( 𝑓 “ ( ℤ ∖ { 0 } ) )
89 cr
90 88 89 74 cinf inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < )
91 90 cneg - inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < )
92 8 91 70 co ( 𝑝 ↑ - inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < ) )
93 86 6 92 cif if ( 𝑓 = ( ℤ × { 0 } ) , 0 , ( 𝑝 ↑ - inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < ) ) )
94 34 30 93 cmpt ( 𝑓𝑏 ↦ if ( 𝑓 = ( ℤ × { 0 } ) , 0 , ( 𝑝 ↑ - inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < ) ) ) )
95 83 94 84 co ( ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) ) } ⟩ } ) toNrmGrp ( 𝑓𝑏 ↦ if ( 𝑓 = ( ℤ × { 0 } ) , 0 , ( 𝑝 ↑ - inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < ) ) ) ) )
96 26 25 95 csb { ∈ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ∣ ∃ 𝑥 ∈ ran ℤ ( “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑏 ( ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) ) } ⟩ } ) toNrmGrp ( 𝑓𝑏 ↦ if ( 𝑓 = ( ℤ × { 0 } ) , 0 , ( 𝑝 ↑ - inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < ) ) ) ) )
97 1 2 96 cmpt ( 𝑝 ∈ ℙ ↦ { ∈ ( ℤ ↑m ( 0 ... ( 𝑝 − 1 ) ) ) ∣ ∃ 𝑥 ∈ ran ℤ ( “ ( ℤ ∖ { 0 } ) ) ⊆ 𝑥 } / 𝑏 ( ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑓f + 𝑔 ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( ( /Qp ‘ 𝑝 ) ‘ ( 𝑛 ∈ ℤ ↦ Σ 𝑘 ∈ ℤ ( ( 𝑓𝑘 ) · ( 𝑔 ‘ ( 𝑛𝑘 ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑏 ∧ Σ 𝑘 ∈ ℤ ( ( 𝑓 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) < Σ 𝑘 ∈ ℤ ( ( 𝑔 ‘ - 𝑘 ) · ( ( 𝑝 + 1 ) ↑ - 𝑘 ) ) ) } ⟩ } ) toNrmGrp ( 𝑓𝑏 ↦ if ( 𝑓 = ( ℤ × { 0 } ) , 0 , ( 𝑝 ↑ - inf ( ( 𝑓 “ ( ℤ ∖ { 0 } ) ) , ℝ , < ) ) ) ) ) )
98 0 97 wceq 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 } ) ) , ℝ , < ) ) ) ) ) )