Description: The neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | re0g | |- 0 = ( 0g ` RRfld ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cncrng | |- CCfld e. CRing |
|
| 2 | crngring | |- ( CCfld e. CRing -> CCfld e. Ring ) |
|
| 3 | ringmnd | |- ( CCfld e. Ring -> CCfld e. Mnd ) |
|
| 4 | 1 2 3 | mp2b | |- CCfld e. Mnd |
| 5 | 0re | |- 0 e. RR |
|
| 6 | ax-resscn | |- RR C_ CC |
|
| 7 | df-refld | |- RRfld = ( CCfld |`s RR ) |
|
| 8 | cnfldbas | |- CC = ( Base ` CCfld ) |
|
| 9 | cnfld0 | |- 0 = ( 0g ` CCfld ) |
|
| 10 | 7 8 9 | ress0g | |- ( ( CCfld e. Mnd /\ 0 e. RR /\ RR C_ CC ) -> 0 = ( 0g ` RRfld ) ) |
| 11 | 4 5 6 10 | mp3an | |- 0 = ( 0g ` RRfld ) |