Theorem padicfval

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

	Ref	Expression
Hypothesis	padicval.j	⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
Assertion	padicfval	⊢ ( 𝑃 ∈ ℙ → ( 𝐽 ‘ 𝑃 ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		padicval.j	⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
2		id	⊢ ( 𝑞 = 𝑃 → 𝑞 = 𝑃 )
3		oveq1	⊢ ( 𝑞 = 𝑃 → ( 𝑞 pCnt 𝑥 ) = ( 𝑃 pCnt 𝑥 ) )
4	3	negeqd	⊢ ( 𝑞 = 𝑃 → - ( 𝑞 pCnt 𝑥 ) = - ( 𝑃 pCnt 𝑥 ) )
5	2 4	oveq12d	⊢ ( 𝑞 = 𝑃 → ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) = ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) )
6	5	ifeq2d	⊢ ( 𝑞 = 𝑃 → if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) = if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) )
7	6	mpteq2dv	⊢ ( 𝑞 = 𝑃 → ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) ) )
8		qex	⊢ ℚ ∈ V
9	8	mptex	⊢ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) ) ∈ V
10	7 1 9	fvmpt	⊢ ( 𝑃 ∈ ℙ → ( 𝐽 ‘ 𝑃 ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) ) )