Theorem cnfld1

Description: One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Assertion	cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		mullid	$$⊢x\in ℂ\to 1x=x$$
3		mulrid	$$⊢x\in ℂ\to x\cdot 1=x$$
4	2 3	jca	$$⊢x\in ℂ\to \left(1x=x\wedge x\cdot 1=x\right)$$
5	4	rgen	$$⊢\forall x\in ℂ\left(1x=x\wedge x\cdot 1=x\right)$$
6	1 5	pm3.2i	$$⊢\left(1\in ℂ\wedge \forall x\in ℂ\left(1x=x\wedge x\cdot 1=x\right)\right)$$
7		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
8		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
9		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
10		eqid	$$⊢1_{{ℂ}_{\mathrm{fld}}}=1_{{ℂ}_{\mathrm{fld}}}$$
11	8 9 10	isringid	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to \left(\left(1\in ℂ\wedge \forall x\in ℂ\left(1x=x\wedge x\cdot 1=x\right)\right)\leftrightarrow 1_{{ℂ}_{\mathrm{fld}}}=1\right)$$
12	7 11	ax-mp	$$⊢\left(1\in ℂ\wedge \forall x\in ℂ\left(1x=x\wedge x\cdot 1=x\right)\right)\leftrightarrow 1_{{ℂ}_{\mathrm{fld}}}=1$$
13	6 12	mpbi	$$⊢1_{{ℂ}_{\mathrm{fld}}}=1$$
14	13	eqcomi	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$