This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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