Theorem re0g

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

	Ref	Expression
Assertion	re0g	⊢ 0 = ( 0g ‘ ℝfld )

Proof

Step	Hyp	Ref	Expression
1		cncrng	⊢ ℂfld ∈ CRing
2		crngring	⊢ ( ℂfld ∈ CRing → ℂfld ∈ Ring )
3		ringmnd	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
4	1 2 3	mp2b	⊢ ℂfld ∈ Mnd
5		0re	⊢ 0 ∈ ℝ
6		ax-resscn	⊢ ℝ ⊆ ℂ
7		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
8		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
9		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
10	7 8 9	ress0g	⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ ℝ ∧ ℝ ⊆ ℂ ) → 0 = ( 0g ‘ ℝfld ) )
11	4 5 6 10	mp3an	⊢ 0 = ( 0g ‘ ℝfld )