Theorem zringplusg

Description: The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017) (Revised by AV, 9-Jun-2019)

	Ref	Expression
Assertion	zringplusg	⊢ + = ( +g ‘ ℤring )

Proof

Step	Hyp	Ref	Expression
1		zex	⊢ ℤ ∈ V
2		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
3		cnfldadd	⊢ + = ( +g ‘ ℂfld )
4	2 3	ressplusg	⊢ ( ℤ ∈ V → + = ( +g ‘ ℤring ) )
5	1 4	ax-mp	⊢ + = ( +g ‘ ℤring )