Theorem padicval

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

	Ref	Expression
Hypothesis	padicval.j	$$⊢J=\left(q\in \mathbb{P}⟼\left(x\in \mathbb{Q}⟼if\left(x=0,0,q^{-\left(q\mathrm{pCnt}x\right)}\right)\right)\right)$$
Assertion	padicval	$$⊢\left(P\in \mathbb{P}\wedge X\in \mathbb{Q}\right)\to J\left(P\right)\left(X\right)=if\left(X=0,0,P^{-\left(P\mathrm{pCnt}X\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		padicval.j	$$⊢J=\left(q\in \mathbb{P}⟼\left(x\in \mathbb{Q}⟼if\left(x=0,0,q^{-\left(q\mathrm{pCnt}x\right)}\right)\right)\right)$$
2	1	padicfval	$$⊢P\in \mathbb{P}\to J\left(P\right)=\left(x\in \mathbb{Q}⟼if\left(x=0,0,P^{-\left(P\mathrm{pCnt}x\right)}\right)\right)$$
3	2	fveq1d	$$⊢P\in \mathbb{P}\to J\left(P\right)\left(X\right)=\left(x\in \mathbb{Q}⟼if\left(x=0,0,P^{-\left(P\mathrm{pCnt}x\right)}\right)\right)\left(X\right)$$
4		eqeq1	$$⊢x=X\to \left(x=0\leftrightarrow X=0\right)$$
5		oveq2	$$⊢x=X\to P\mathrm{pCnt}x=P\mathrm{pCnt}X$$
6	5	negeqd	$$⊢x=X\to -\left(P\mathrm{pCnt}x\right)=-\left(P\mathrm{pCnt}X\right)$$
7	6	oveq2d	$$⊢x=X\to P^{-\left(P\mathrm{pCnt}x\right)}=P^{-\left(P\mathrm{pCnt}X\right)}$$
8	4 7	ifbieq2d	$$⊢x=X\to if\left(x=0,0,P^{-\left(P\mathrm{pCnt}x\right)}\right)=if\left(X=0,0,P^{-\left(P\mathrm{pCnt}X\right)}\right)$$
9		eqid	$$⊢\left(x\in \mathbb{Q}⟼if\left(x=0,0,P^{-\left(P\mathrm{pCnt}x\right)}\right)\right)=\left(x\in \mathbb{Q}⟼if\left(x=0,0,P^{-\left(P\mathrm{pCnt}x\right)}\right)\right)$$
10		c0ex	$$⊢0\in \mathrm{V}$$
11		ovex	$$⊢P^{-\left(P\mathrm{pCnt}X\right)}\in \mathrm{V}$$
12	10 11	ifex	$$⊢if\left(X=0,0,P^{-\left(P\mathrm{pCnt}X\right)}\right)\in \mathrm{V}$$
13	8 9 12	fvmpt	$$⊢X\in \mathbb{Q}\to \left(x\in \mathbb{Q}⟼if\left(x=0,0,P^{-\left(P\mathrm{pCnt}x\right)}\right)\right)\left(X\right)=if\left(X=0,0,P^{-\left(P\mathrm{pCnt}X\right)}\right)$$
14	3 13	sylan9eq	$$⊢\left(P\in \mathbb{P}\wedge X\in \mathbb{Q}\right)\to J\left(P\right)\left(X\right)=if\left(X=0,0,P^{-\left(P\mathrm{pCnt}X\right)}\right)$$