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 e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
Assertion padicval 
|- ( ( P e. Prime /\ X e. QQ ) -> ( ( J ` P ) ` X ) = 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 1 padicfval 
 |-  ( P e. Prime -> ( J ` P ) = ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) ) )
3 2 fveq1d 
 |-  ( P e. Prime -> ( ( J ` P ) ` X ) = ( ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( 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 -> -u ( P pCnt x ) = -u ( P pCnt X ) )
7 6 oveq2d 
 |-  ( x = X -> ( P ^ -u ( P pCnt x ) ) = ( P ^ -u ( P pCnt X ) ) )
8 4 7 ifbieq2d 
 |-  ( x = X -> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) = if ( X = 0 , 0 , ( P ^ -u ( P pCnt X ) ) ) )
9 eqid 
 |-  ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) ) = ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) )
10 c0ex 
 |-  0 e. _V
11 ovex 
 |-  ( P ^ -u ( P pCnt X ) ) e. _V
12 10 11 ifex 
 |-  if ( X = 0 , 0 , ( P ^ -u ( P pCnt X ) ) ) e. _V
13 8 9 12 fvmpt 
 |-  ( X e. QQ -> ( ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) ) ` X ) = if ( X = 0 , 0 , ( P ^ -u ( P pCnt X ) ) ) )
14 3 13 sylan9eq 
 |-  ( ( P e. Prime /\ X e. QQ ) -> ( ( J ` P ) ` X ) = if ( X = 0 , 0 , ( P ^ -u ( P pCnt X ) ) ) )