Definition df-zp

Description: Define the p -adic integers, as a subset of the p -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-zp	$$⊢{\mathbb{Z}}_p=\mathrm{\mathbb{Z}Ring}\circ {\mathbb{Q}}_p$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czp	$$class{\mathbb{Z}}_p$$
1		czr	$$class\mathrm{\mathbb{Z}Ring}$$
2		cqp	$$class{\mathbb{Q}}_p$$
3	1 2	ccom	$$class\left(\mathrm{\mathbb{Z}Ring}\circ {\mathbb{Q}}_p\right)$$
4	0 3	wceq	$$wff{\mathbb{Z}}_p=\mathrm{\mathbb{Z}Ring}\circ {\mathbb{Q}}_p$$