Theorem zringsubgval

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

	Ref	Expression
Hypothesis	zringsubgval.m	⊢ − = ( -g ‘ ℤring )
Assertion	zringsubgval	⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		zringsubgval.m	⊢ − = ( -g ‘ ℤring )
2		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
3		subrgsubg	⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
4	2 3	ax-mp	⊢ ℤ ∈ ( SubGrp ‘ ℂfld )
5		cnfldsub	⊢ − = ( -g ‘ ℂfld )
6		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
7	5 6 1	subgsub	⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )
8	4 7	mp3an1	⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )