Theorem zringsubgval

Description: Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019)

	Ref	Expression
Hypothesis	zringsubgval.m	|- .- = ( -g ` ZZring )
Assertion	zringsubgval	|- ( ( X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )

Proof

Step	Hyp	Ref	Expression
1		zringsubgval.m	|- .- = ( -g ` ZZring )
2		zsubrg	|- ZZ e. ( SubRing ` CCfld )
3		subrgsubg	|- ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubGrp ` CCfld ) )
4	2 3	ax-mp	|- ZZ e. ( SubGrp ` CCfld )
5		cnfldsub	|- - = ( -g ` CCfld )
6		df-zring	|- ZZring = ( CCfld |`s ZZ )
7	5 6 1	subgsub	|- ( ( ZZ e. ( SubGrp ` CCfld ) /\ X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )
8	4 7	mp3an1	|- ( ( X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )