Theorem cnsrng

Description: The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Assertion	cnsrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
2	1	a1i	$$⊢\top \to ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
3		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
4	3	a1i	$$⊢\top \to +={+}_{{ℂ}_{\mathrm{fld}}}$$
5		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
6	5	a1i	$$⊢\top \to \times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
7		cnfldcj	$$⊢*={\mathrm{*}}_{{ℂ}_{\mathrm{fld}}}$$
8	7	a1i	$$⊢\top \to *={\mathrm{*}}_{{ℂ}_{\mathrm{fld}}}$$
9		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
10	9	a1i	$$⊢\top \to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
11		cjcl	$$⊢x\in ℂ\to \bar{x}\in ℂ$$
12	11	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \bar{x}\in ℂ$$
13		cjadd	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \overline{x+y}=\bar{x}+\bar{y}$$
14	13	3adant1	$$⊢\left(\top \wedge x\in ℂ\wedge y\in ℂ\right)\to \overline{x+y}=\bar{x}+\bar{y}$$
15		mulcom	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to xy=yx$$
16	15	fveq2d	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \overline{xy}=\overline{yx}$$
17		cjmul	$$⊢\left(y\in ℂ\wedge x\in ℂ\right)\to \overline{yx}=\bar{y}\bar{x}$$
18	17	ancoms	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \overline{yx}=\bar{y}\bar{x}$$
19	16 18	eqtrd	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \overline{xy}=\bar{y}\bar{x}$$
20	19	3adant1	$$⊢\left(\top \wedge x\in ℂ\wedge y\in ℂ\right)\to \overline{xy}=\bar{y}\bar{x}$$
21		cjcj	$$⊢x\in ℂ\to \overline{\stackrel{‾}{x}}=x$$
22	21	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \overline{\stackrel{‾}{x}}=x$$
23	2 4 6 8 10 12 14 20 22	issrngd	$$⊢\top \to {ℂ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$
24	23	mptru	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$