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 |