Theorem cnfld1

Description: One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) Avoid ax-mulf . (Revised by GG, 31-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		ovmpot	$$⊢\left(1\in ℂ\wedge x\in ℂ\right)\to 1\left(u\in ℂ,v\in ℂ⟼uv\right)x=1x$$
3	2	eqcomd	$$⊢\left(1\in ℂ\wedge x\in ℂ\right)\to 1x=1\left(u\in ℂ,v\in ℂ⟼uv\right)x$$
4	1 3	mpan	$$⊢x\in ℂ\to 1x=1\left(u\in ℂ,v\in ℂ⟼uv\right)x$$
5		mullid	$$⊢x\in ℂ\to 1x=x$$
6	4 5	eqtr3d	$$⊢x\in ℂ\to 1\left(u\in ℂ,v\in ℂ⟼uv\right)x=x$$
7		ovmpot	$$⊢\left(x\in ℂ\wedge 1\in ℂ\right)\to x\left(u\in ℂ,v\in ℂ⟼uv\right)1=x\cdot 1$$
8	1 7	mpan2	$$⊢x\in ℂ\to x\left(u\in ℂ,v\in ℂ⟼uv\right)1=x\cdot 1$$
9		mulrid	$$⊢x\in ℂ\to x\cdot 1=x$$
10	8 9	eqtrd	$$⊢x\in ℂ\to x\left(u\in ℂ,v\in ℂ⟼uv\right)1=x$$
11	6 10	jca	$$⊢x\in ℂ\to \left(1\left(u\in ℂ,v\in ℂ⟼uv\right)x=x\wedge x\left(u\in ℂ,v\in ℂ⟼uv\right)1=x\right)$$
12	11	rgen	$$⊢\forall x\in ℂ\left(1\left(u\in ℂ,v\in ℂ⟼uv\right)x=x\wedge x\left(u\in ℂ,v\in ℂ⟼uv\right)1=x\right)$$
13	1 12	pm3.2i	$$⊢\left(1\in ℂ\wedge \forall x\in ℂ\left(1\left(u\in ℂ,v\in ℂ⟼uv\right)x=x\wedge x\left(u\in ℂ,v\in ℂ⟼uv\right)1=x\right)\right)$$
14		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
15		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
16		mpocnfldmul	$$⊢\left(u\in ℂ,v\in ℂ⟼uv\right)={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
17		eqid	$$⊢1_{{ℂ}_{\mathrm{fld}}}=1_{{ℂ}_{\mathrm{fld}}}$$
18	15 16 17	isringid	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to \left(\left(1\in ℂ\wedge \forall x\in ℂ\left(1\left(u\in ℂ,v\in ℂ⟼uv\right)x=x\wedge x\left(u\in ℂ,v\in ℂ⟼uv\right)1=x\right)\right)\leftrightarrow 1_{{ℂ}_{\mathrm{fld}}}=1\right)$$
19	14 18	ax-mp	$$⊢\left(1\in ℂ\wedge \forall x\in ℂ\left(1\left(u\in ℂ,v\in ℂ⟼uv\right)x=x\wedge x\left(u\in ℂ,v\in ℂ⟼uv\right)1=x\right)\right)\leftrightarrow 1_{{ℂ}_{\mathrm{fld}}}=1$$
20	13 19	mpbi	$$⊢1_{{ℂ}_{\mathrm{fld}}}=1$$
21	20	eqcomi	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$