Metamath Proof Explorer

Theorem padicfval

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

Ref Expression
Hypothesis padicval.j 
|- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
Assertion padicfval 
|- ( P e. Prime -> ( J ` P ) = ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 padicval.j 
 |-  J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
2 id 
 |-  ( q = P -> q = P )
3 oveq1 
 |-  ( q = P -> ( q pCnt x ) = ( P pCnt x ) )
4 3 negeqd 
 |-  ( q = P -> -u ( q pCnt x ) = -u ( P pCnt x ) )
5 2 4 oveq12d 
 |-  ( q = P -> ( q ^ -u ( q pCnt x ) ) = ( P ^ -u ( P pCnt x ) ) )
6 5 ifeq2d 
 |-  ( q = P -> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) = if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) )
7 6 mpteq2dv 
 |-  ( q = P -> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) = ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) ) )
8 qex 
 |-  QQ e. _V
9 8 mptex 
 |-  ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) ) e. _V
10 7 1 9 fvmpt 
 |-  ( P e. Prime -> ( J ` P ) = ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) ) )