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
|- RRfld e. *Ring

Proof

Step Hyp Ref Expression
1 rebase
 |-  RR = ( Base ` RRfld )
2 refldcj
 |-  * = ( *r ` RRfld )
3 refld
 |-  RRfld e. Field
4 3 a1i
 |-  ( T. -> RRfld e. Field )
5 4 fldcrngd
 |-  ( T. -> RRfld e. CRing )
6 cjre
 |-  ( x e. RR -> ( * ` x ) = x )
7 6 adantl
 |-  ( ( T. /\ x e. RR ) -> ( * ` x ) = x )
8 1 2 5 7 idsrngd
 |-  ( T. -> RRfld e. *Ring )
9 8 mptru
 |-  RRfld e. *Ring