Metamath Proof Explorer

Theorem recrng

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

Ref Expression
Assertion recrng 
|- RRfld e. *Ring

Proof

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