Theorem zringsubgval

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

	Ref	Expression
Hypothesis	zringsubgval.m	$$⊢\underset{\dot{}}{-}={-}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
Assertion	zringsubgval	$$⊢\left(X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)\to X-Y=X\underset{\dot{}}{-}Y$$

Proof

Step	Hyp	Ref	Expression
1		zringsubgval.m	$$⊢\underset{\dot{}}{-}={-}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
2		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
3		subrgsubg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
4	2 3	ax-mp	$$⊢\mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
5		cnfldsub	$$⊢-={-}_{{ℂ}_{\mathrm{fld}}}$$
6		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
7	5 6 1	subgsub	$$⊢\left(\mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)\to X-Y=X\underset{\dot{}}{-}Y$$
8	4 7	mp3an1	$$⊢\left(X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)\to X-Y=X\underset{\dot{}}{-}Y$$