Theorem padicfval

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	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)$$

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		id	$$⊢q=P\to q=P$$
3		oveq1	$$⊢q=P\to q\mathrm{pCnt}x=P\mathrm{pCnt}x$$
4	3	negeqd	$$⊢q=P\to -\left(q\mathrm{pCnt}x\right)=-\left(P\mathrm{pCnt}x\right)$$
5	2 4	oveq12d	$$⊢q=P\to q^{-\left(q\mathrm{pCnt}x\right)}=P^{-\left(P\mathrm{pCnt}x\right)}$$
6	5	ifeq2d	$$⊢q=P\to if\left(x=0,0,q^{-\left(q\mathrm{pCnt}x\right)}\right)=if\left(x=0,0,P^{-\left(P\mathrm{pCnt}x\right)}\right)$$
7	6	mpteq2dv	$$⊢q=P\to \left(x\in \mathbb{Q}⟼if\left(x=0,0,q^{-\left(q\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)$$
8		qex	$$⊢\mathbb{Q}\in \mathrm{V}$$
9	8	mptex	$$⊢\left(x\in \mathbb{Q}⟼if\left(x=0,0,P^{-\left(P\mathrm{pCnt}x\right)}\right)\right)\in \mathrm{V}$$
10	7 1 9	fvmpt	$$⊢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)$$