Metamath Proof Explorer


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