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	⊢ ℝfld ∈ *-Ring

Proof

Step	Hyp	Ref	Expression
1		rebase	⊢ ℝ = ( Base ‘ ℝfld )
2		refldcj	⊢ ∗ = ( *𝑟 ‘ ℝfld )
3		refld	⊢ ℝfld ∈ Field
4	3	a1i	⊢ ( ⊤ → ℝfld ∈ Field )
5	4	fldcrngd	⊢ ( ⊤ → ℝfld ∈ CRing )
6		cjre	⊢ ( 𝑥 ∈ ℝ → ( ∗ ‘ 𝑥 ) = 𝑥 )
7	6	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( ∗ ‘ 𝑥 ) = 𝑥 )
8	1 2 5 7	idsrngd	⊢ ( ⊤ → ℝfld ∈ *-Ring )
9	8	mptru	⊢ ℝfld ∈ *-Ring