Theorem recrng

Description: The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019)

	Ref	Expression
Assertion	recrng	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$

Proof

Step	Hyp	Ref	Expression
1		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
2		refldcj	$$⊢*={\mathrm{*}}_{{ℝ}_{\mathrm{fld}}}$$
3		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
4		isfld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\leftrightarrow \left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\right)$$
5	3 4	mpbi	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\right)$$
6	5	simpri	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CRing}$$
7	6	a1i	$$⊢\top \to {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}$$
8		cjre	$$⊢x\in ℝ\to \bar{x}=x$$
9	8	adantl	$$⊢\left(\top \wedge x\in ℝ\right)\to \bar{x}=x$$
10	1 2 7 9	idsrngd	$$⊢\top \to {ℝ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$
11	10	mptru	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$