Theorem re0g

Description: The neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)

	Ref	Expression
Assertion	re0g	$$⊢0=0_{{ℝ}_{\mathrm{fld}}}$$

Proof

Step	Hyp	Ref	Expression
1		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
2		crngring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
3		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
4	1 2 3	mp2b	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
5		0re	$$⊢0\in ℝ$$
6		ax-resscn	$$⊢ℝ\subseteq ℂ$$
7		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
8		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
9		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
10	7 8 9	ress0g	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in ℝ\wedge ℝ\subseteq ℂ\right)\to 0=0_{{ℝ}_{\mathrm{fld}}}$$
11	4 5 6 10	mp3an	$$⊢0=0_{{ℝ}_{\mathrm{fld}}}$$