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 } ) ) , ℝ , < ) ) ) ) ) )