zringsubgval

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

		Ref	Expression
	Hypothesis	zringsubgval.m	$⊢ \underset{˙}{-} = -_{ℤ_{ring}}$
	Assertion	zringsubgval	$⊢ (X \in ℤ \land Y \in ℤ) \to X - Y = X \underset{˙}{-} Y$

Step	Hyp	Ref	Expression
1		zringsubgval.m	$⊢ \underset{˙}{-} = -_{ℤ_{ring}}$
2		zsubrg	$⊢ ℤ \in SubRing (ℂ_{fld})$
3		subrgsubg	$⊢ ℤ \in SubRing (ℂ_{fld}) \to ℤ \in SubGrp (ℂ_{fld})$
4	2 3	ax-mp	$⊢ ℤ \in SubGrp (ℂ_{fld})$
5		cnfldsub	$⊢ - = -_{ℂ_{fld}}$
6		df-zring	$⊢ ℤ_{ring} = ℂ_{fld} ↾_{𝑠} ℤ$
7	5 6 1	subgsub	$⊢ (ℤ \in SubGrp (ℂ_{fld}) \land X \in ℤ \land Y \in ℤ) \to X - Y = X \underset{˙}{-} Y$
8	4 7	mp3an1	$⊢ (X \in ℤ \land Y \in ℤ) \to X - Y = X \underset{˙}{-} Y$

Metamath Proof Explorer