Theorem padicval

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	padicval	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ ) → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑋 ) = if ( 𝑋 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		padicval.j	⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
2	1	padicfval	⊢ ( 𝑃 ∈ ℙ → ( 𝐽 ‘ 𝑃 ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) ) )
3	2	fveq1d	⊢ ( 𝑃 ∈ ℙ → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) ) ‘ 𝑋 ) )
4		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 0 ↔ 𝑋 = 0 ) )
5		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑃 pCnt 𝑥 ) = ( 𝑃 pCnt 𝑋 ) )
6	5	negeqd	⊢ ( 𝑥 = 𝑋 → - ( 𝑃 pCnt 𝑥 ) = - ( 𝑃 pCnt 𝑋 ) )
7	6	oveq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) = ( 𝑃 ↑ - ( 𝑃 pCnt 𝑋 ) ) )
8	4 7	ifbieq2d	⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) = if ( 𝑋 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑋 ) ) ) )
9		eqid	⊢ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) ) = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) )
10		c0ex	⊢ 0 ∈ V
11		ovex	⊢ ( 𝑃 ↑ - ( 𝑃 pCnt 𝑋 ) ) ∈ V
12	10 11	ifex	⊢ if ( 𝑋 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑋 ) ) ) ∈ V
13	8 9 12	fvmpt	⊢ ( 𝑋 ∈ ℚ → ( ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑥 ) ) ) ) ‘ 𝑋 ) = if ( 𝑋 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑋 ) ) ) )
14	3 13	sylan9eq	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ ) → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑋 ) = if ( 𝑋 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑋 ) ) ) )