Theorem resrng

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

	Ref	Expression
Assertion	resrng	$$⊢{ℝ}_{\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	3	a1i	$$⊢\top \to {ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
5	4	fldcrngd	$$⊢\top \to {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}$$
6		cjre	$$⊢x\in ℝ\to \bar{x}=x$$
7	6	adantl	$$⊢\left(\top \wedge x\in ℝ\right)\to \bar{x}=x$$
8	1 2 5 7	idsrngd	$$⊢\top \to {ℝ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$
9	8	mptru	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$