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 |
| 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 |