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 ` ZZring )

Proof

Step	Hyp	Ref	Expression
1		zex	|- ZZ e. _V
2		df-zring	|- ZZring = ( CCfld |`s ZZ )
3		cnfldadd	|- + = ( +g ` CCfld )
4	2 3	ressplusg	|- ( ZZ e. _V -> + = ( +g ` ZZring ) )
5	1 4	ax-mp	|- + = ( +g ` ZZring )