Metamath Proof Explorer

Theorem padicval

Description: Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypothesis padicval.j ⊢ J = q ∈ ℙ ⟼ x ∈ ℚ ⟼ if x = 0 0 q − q pCnt x
Assertion padicval ⊢ P ∈ ℙ ∧ X ∈ ℚ → J ⁡ P ⁡ X = if X = 0 0 P − P pCnt X

Proof

Step Hyp Ref Expression
1 padicval.j ⊢ J = q ∈ ℙ ⟼ x ∈ ℚ ⟼ if x = 0 0 q − q pCnt x
2 1 padicfval ⊢ P ∈ ℙ → J ⁡ P = x ∈ ℚ ⟼ if x = 0 0 P − P pCnt x
3 2 fveq1d ⊢ P ∈ ℙ → J ⁡ P ⁡ X = x ∈ ℚ ⟼ if x = 0 0 P − P pCnt x ⁡ X
4 eqeq1 ⊢ x = X → x = 0 ↔ X = 0
5 oveq2 ⊢ x = X → P pCnt x = P pCnt X
6 5 negeqd ⊢ x = X → − P pCnt x = − P pCnt X
7 6 oveq2d ⊢ x = X → P − P pCnt x = P − P pCnt X
8 4 7 ifbieq2d ⊢ x = X → if x = 0 0 P − P pCnt x = if X = 0 0 P − P pCnt X
9 eqid ⊢ x ∈ ℚ ⟼ if x = 0 0 P − P pCnt x = x ∈ ℚ ⟼ if x = 0 0 P − P pCnt x
10 c0ex ⊢ 0 ∈ V
11 ovex ⊢ P − P pCnt X ∈ V
12 10 11 ifex ⊢ if X = 0 0 P − P pCnt X ∈ V
13 8 9 12 fvmpt ⊢ X ∈ ℚ → x ∈ ℚ ⟼ if x = 0 0 P − P pCnt x ⁡ X = if X = 0 0 P − P pCnt X
14 3 13 sylan9eq ⊢ P ∈ ℙ ∧ X ∈ ℚ → J ⁡ P ⁡ X = if X = 0 0 P − P pCnt X