Definition df-cp

Description: Define the metric completion of the algebraic completion of the p -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-cp	$$⊢{ℂ}_p=\mathrm{cplMetSp}\circ \overline{{\mathbb{Q}}_p}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccp	$$class{ℂ}_p$$
1		ccpms	$$class\mathrm{cplMetSp}$$
2		cqpa	$$class\overline{{\mathbb{Q}}_p}$$
3	1 2	ccom	$$class\left(\mathrm{cplMetSp}\circ \overline{{\mathbb{Q}}_p}\right)$$
4	0 3	wceq	$$wff{ℂ}_p=\mathrm{cplMetSp}\circ \overline{{\mathbb{Q}}_p}$$